Google DeepMind announced on November 10 that a team of AI agents has mathematically proved key security properties of the actual code underlying the Signal protocol, the encryption technology that protects billions of private conversations in apps such as Signal and Google Messages. DeepMind called it a milestone long considered a grand challenge.
The work was done with AlphaProof Code, a new multi-agent framework for formal verification. Formal verification means mathematically proving that code behaves as specified, without flaws, and it is regarded as the highest standard of security assurance. It is also difficult and labor-intensive, which is why most protocols have been formally analyzed only at the design level, not in the compiled code that runs on devices.
DeepMind said this is the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time the implementation of a widely deployed protocol of this kind has been formally verified by any method, with or without AI. That matters, because vulnerabilities often hide in the gap between a sound design and its implementation.
The process split the work the way a research team would. Human experts worked with a mix of models to translate Signal's security goals into formal mathematical specifications, and human experts reviewed every specification. Agents powered by Gemini Carbon then carried out the proofs, generating over six million lines of Lean, a language used to construct machine-checked mathematical proofs of code.
When the proofs were complete, the agents audited their own work and flagged areas needing a human second look. DeepMind said that was just one percent of the codebase. Because Lean automatically checks the rest, experts could focus where human judgment mattered most.
Even at that complexity, the whole verification took just four weeks, a task DeepMind said has historically taken expert teams years. The proofs covered properties such as keeping messages protected before and after a device is temporarily compromised, and they held down to the exact compiled code running on devices, not just to an abstract description of the protocol.
To test whether the system could tell sound code from faulty code, the researchers reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, AlphaProof Code produced a machine-checked proof that the buggy version was insecure. A tool that passes everything would prove nothing.
DeepMind is open-sourcing its formal verification artifacts for community use, so other researchers can inspect the specifications and proofs for themselves. The research was led by Pushmeet Kohli and Swarat Chaudhuri. Signal staff, including Ehren Kret, gave feedback on the methodology.
The result does not mean every part of every messaging app is now proven sound. The proofs cover Signal's core cryptographic code and the security properties the experts specified, which is a narrower and more meaningful claim. It does, however, lay groundwork that DeepMind says could extend to other vital systems, from medical device firmware to power grid software.
DeepMind also linked the work to automated defense tools such as CodeMender, arguing that formal verification paired with defense agents could help defenders keep pace with the speed and scale of modern, increasingly AI-driven cyber threats. If it scales, mathematical proof could become a practical part of how critical software is shipped.