Google DeepMind published a research post on November 10, 2026 describing AlphaProof Code, an agentic framework that the authors say helped mathematically prove key security properties of the actual code behind the Signal protocol. The post is bylined Pushmeet Kohli and Swarat Chaudhuri. They called formal verification of a widely deployed cryptographic protocol at this depth a long-standing challenge, and said this was the first time artificial intelligence had been used to do so. They also said it was the first time the implementation of a widely deployed protocol of this kind had been formally verified by any method, with or without AI.
The Signal protocol protects private conversations in apps such as Signal and Google Messages, the authors wrote. Most prior verification work, they said, has stopped at the design of a protocol rather than at the compiled code that runs on devices. AlphaProof Code is described as splitting the labor the way a research team would: human experts work with models to decide what should be proved, then a group of agents carries out the proofs.
DeepMind said its researchers collaborated with a mix of models to translate Signal's security goals into formal mathematical specifications, with human experts reviewing every specification. Agents powered by Gemini Carbon then generated more than six million lines of Lean, a language used to write machine-checked mathematical proofs. The agents also audited the proof and flagged about one percent of the codebase for a second human look. Because Lean checks the rest automatically, the authors wrote, experts could concentrate their review where judgment still matters.
The agents were used to prove that the compiled code meets specified properties, including keeping messages protected before and after a device is temporarily compromised. The authors said the process took four weeks, compared with work that historically takes expert teams years. To test whether the system can tell correct code from faulty code, they reintroduced two real bugs that had already been fixed into an isolated version of Signal's code. In both cases, they said, the system produced a machine-checked proof that the buggy version was insecure.
Ehren Kret, chief technology officer of Signal, is quoted as saying that prior formal verification had focused on smaller portions of the code and that using AI agents to translate live code into valid Lean theorems is a major breakthrough. He said that as AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives Signal greater confidence in its privacy guarantees. DeepMind listed additional Signal staff, including Rolfe Schmidt and Michael Rosenberg, among those who gave feedback on the methodology.
The authors framed the result as a step toward bringing this kind of assurance to other critical software, from medical-device firmware to power-grid systems, and said they are open-sourcing formal verification artifacts for community use. They also pointed readers to a technical paper on the same page. The work sits alongside Google's same-day launch of Gemini 4 Carbon, which the Carbon announcement cites as the model used with other systems inside AlphaProof Code. The two posts are related but describe different events: one is a research result about Signal's code, the other is a product-availability change.
The claims about novelty, the four-week timeline, the six million lines of Lean and the two reintroduced bugs all come from DeepMind, supported by Signal's quoted endorsement of the approach. This reporting did not independently re-run the proofs or audit the open-sourced artifacts. Readers should treat those figures and the historical comparison with multi-year expert efforts as the authors' account, and should note that the verification covers key specified properties of the protocol implementation rather than an unbounded promise that every possible flaw has been ruled out.