Google DeepMind on November 10, 2026 introduced AlphaProof Code, an agentic framework for formal software verification, and said it used the system to formally verify code from Signal's cryptographic protocol. That protocol secures private messaging in Signal and Google Messages. DeepMind says this is the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth.
According to the announcement, written by Pushmeet Kohli and Swarat Chaudhuri, the work had three stages. Researchers used several models to turn Signal's security goals into formal specifications, and human experts reviewed each one. Agents running on Gemini Carbon then wrote the proofs, producing more than six million lines of Lean, a language whose proofs are checked mathematically by machine. The agents also audited their own work and flagged about one percent of the codebase for human review. Lean checked the rest automatically.
The proofs cover the compiled code that runs on devices, not only the protocol's design. One property DeepMind gives as an example is keeping messages protected before and after a device is temporarily compromised. The verification took four weeks.
To test whether the system catches real flaws, the team put two previously fixed bugs back into an isolated copy of Signal's code. In both cases AlphaProof Code produced a machine-checked proof that the buggy version was insecure. Signal's CTO, Ehren Kret, is quoted in the announcement, and Signal staff gave feedback on the method.
DeepMind is open-sourcing its formal verification artifacts at google-deepmind.github.io/code-verification and has published a technical paper. The company has not announced a product or access program for AlphaProof Code itself. For teams building security-critical software, the result is an example of AI agents handling the large volume of proof work in formal verification, with people focusing on the specifications and the small share of proofs the agents flag.