DeepMind's AlphaProof Code verifies Signal protocol in four weeks

Google DeepMind's new AlphaProof Code system formally verified selected security guarantees of the Signal protocol in about four weeks, work the company says has historically taken expert teams years. As Wired reported, the agentic framework proved properties of libsignal, Signal's reference implementation, at the machine-code level, covering forward secrecy, authentication, post-compromise security and handshake secrecy.

The framework "combines human expertise with AI agents," according to DeepMind researchers. A five-person team paired with agents powered by Gemini Carbon generated roughly 6.5 million lines of proof code in Lean, with the agents auditing their own work and flagging around 1% for human review. To stress-test the system, the team reintroduced two previously fixed Signal bugs; AlphaProof Code caught both and showed that the protocol could not be formally verified while those issues remained.

The scope is narrower than the framing implies. The proofs cover session establishment via PQXDH in one-to-one communication and the Triple Ratchet protocol that handles sending and receiving messages. They assume perfect cryptography and leave the full Signal mobile app unverified. Google told Wired "it's unclear as yet how practical it will be to use it more broadly," given the compute demands of agentic formal verification.

DeepMind has open-sourced the verification artifacts and published a technical paper alongside the announcement. The team is claiming two firsts: the first AI-assisted formal verification of a widely deployed cryptographic protocol at this depth, and "the first time any method has verified a protocol's actual running implementation, as opposed to just its design blueprint."