Google DeepMind on November 10, 2026 introduced AlphaProof Code, an agentic framework for formal software verification, and said researchers used it to mathematically prove key security properties of the actual code behind the Signal protocol. That protocol protects private messages in Signal and Google Messages, among other apps. Formal verification means producing a mathematical proof that software behaves as specified, and it is widely regarded as the strongest form of security assurance, but it has historically demanded so much expert labor that it is rarely applied to large real-world codebases.
DeepMind describes AlphaProof Code as a multi-model system that divides the work the way a research team would. Human experts work with AI models to translate a system's security goals into formal specifications, reviewing each one. Once a specification is approved, a group of autonomous prover agents, powered by Gemini Carbon according to DeepMind, writes proofs in Lean, a language whose kernel mechanically checks every step. Proofs are accepted only if Lean confirms them against the approved specification. The agents then audit their own work and flag areas for a closer human look; DeepMind says that came to about one percent of the codebase.
According to the accompanying technical paper, the team targeted libsignal, Signal's reference implementation, compiled with the standard Rust compiler to AArch64 machine code. The proofs cover the post-quantum PQXDH handshake and the Triple Ratchet messaging scheme, establishing properties including forward secrecy, authentication, post-compromise security, and handshake secrecy. The paper reports about 6.5 million lines of machine-checked Lean proof resting on roughly 26,000 lines of trusted specifications and machine-code semantics. DeepMind says the work took four weeks and calls it the first time the implementation of a widely deployed protocol like this has been formally verified by any method. These characterizations are DeepMind's own.
To show the system can tell sound code from flawed code, the researchers reintroduced two real, previously fixed bugs into an isolated copy of Signal's code; DeepMind says AlphaProof Code produced machine-checked proofs that the altered versions were insecure. Signal CTO Ehren Kret said in DeepMind's announcement that using AI agents to turn live code into valid Lean theorems is a major breakthrough that gives Signal greater confidence in its privacy guarantees.
Independent coverage adds important context. WIRED reported that the analysis found no new vulnerabilities in the portions of Signal it examined, did not cover the entire Signal app, and was done free of charge as a research project; Google declined to share its cost or say whether a commercial product is planned. The Register noted that parts of the result assume idealized cryptographic primitives, so it is a strong statement of correctness rather than a guarantee about every byte. Axios also reported the announcement, citing a different proof-line count than DeepMind's own materials. DeepMind says it is open-sourcing its specifications and proofs, and frames the work as a step toward verifying other critical systems such as medical device firmware and power grid software.