Google DeepMind said on November 10, 2026, that its AI agents formally verified the compiled code behind the Signal protocol, the encryption that protects billions of private conversations in Signal and Google Messages. The work took four weeks. DeepMind says it is the first time the implementation of a widely deployed protocol has been formally verified by any method, with or without AI, and the first time AI has done it at this depth.
What DeepMind actually proved
The target was libsignal version 0.105.4 with SPQR version 1.6.0, compiled with stock rustc 1.98.1, statically linked against musl, and emitted as a single AArch64 Linux executable, according to the technical paper published with the announcement. The agents verified roughly 560 kilobytes of libsignal source, about 140,000 AArch64 instructions, by writing a Lean model of the instruction set covering 467 instructions and 31 system calls in 7,578 lines, then proving that the real executable, loaded and run under that model, preserves the security properties. Ten symbolic theorems cover forward secrecy, post-compromise security, initiator and responder secrecy, authentication, and five corollaries of PQXDH's Theorem 1, and the main result is named signal_session_secure_placed. In plain terms, the proof covers the post-quantum PQXDH handshake and the Triple Ratchet, and it covers the handshake, sending, and receiving in one-to-one sessions.
| Proved | Not proved |
| The compiled code, not just the design, keeps the promised properties | The whole Signal app, which was never the target |
| Forward secrecy and post-compromise security for one-to-one sessions | Group messaging, which sits outside the verified scope |
| Authentication and handshake secrecy under the PQXDH handshake | Key generation, which the proof does not cover |
| Two real, previously fixed bugs are caught when reintroduced | Multi-device state, which the proof does not cover |
| Properties hold down to the exact code running on devices | Security against a quantum attacker in the computational sense, which the paper does not establish for SPQR's healing property |
The distinction in the first row is the whole story. Most protocol verification stops at the design: experts prove that the protocol, as written on paper, has the right properties. DeepMind's agents went further and proved that the compiled code fulfills them, down to the exact code running on devices. Real-world vulnerabilities often hide in the gap between design and implementation, and bridging that gap is what makes these proofs vastly more complex, DeepMind said.
The proof, by the numbers
Agents powered by Gemini Carbon generated more than six million lines of Lean, the computer language that mathematically proves the accuracy of code, including more than three million lines of machine-checked proof, according to DeepMind. The technical paper puts the total at 6.5 million lines of Lean, counting comments and blank lines, according to The Register. The trusted base the proof stands on is far smaller: about 26,000 lines of specification and machine semantics that humans have to trust, according to the paper. The agents audited their own proof and flagged about 1 percent of the codebase for a second human look, and human experts reviewed every specification before the agents started. The verification took four weeks, against years for expert teams historically, according to DeepMind, a comparison the company states without a matched human-only experiment to anchor it.
How the agents did it
Formal verification means proving, mathematically, that code does what it is supposed to do, with no flaws in the logic. It is the highest standard of security assurance, and it is usually slow, manual work that takes expert teams years. AlphaProof Code splits the job the way a research team would. Human experts work with a mix of models to decide what must be true, translating Signal's security goals into formal mathematical specifications, and human experts review every one. Then a group of AI agents does the proving, writing the proofs in Lean, a language whose checker mechanically confirms each step. Because Lean automatically checks the rest, the experts focus their review where human judgment matters most. To confirm that the system can tell correct code from buggy code, the team reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure.
What it did not prove
The proof is real, and its limits are stated in the paper. The theorems hold only for the operations and assumptions the paper lists. The ratchet theorems assume the attacker chooses the SPQR keys, so no post-quantum guarantee is established for SPQR's healing property. The proofs assume idealized cryptographic primitives and the soundness of Lean's kernel and the modelled AArch64 semantics. That means the result does not guarantee the computational secrecy of bytes, and it does not make Signal unbreakable. It proves that specific, human-approved security properties hold in the core cryptographic code, for the sessions and operations listed, under the assumptions listed. Signal and Google Messages users have nothing to install, and the result changes nothing about how the apps work. What changes is the evidence behind them: the core cryptography now carries a machine-checked proof instead of only expert review.
Why this matters beyond Signal
DeepMind says verifying Signal's core cryptography lays the groundwork for securing other vital systems, from medical device firmware to power grid software, and that paired with automated defense agents like CodeMender, formal verification can help counter the speed and scale of modern cyber threats. WIRED reported that DeepMind did the Signal analysis free of charge as a research project, that Google declined to share what it cost, and that the company would not say whether a commercial verification product is coming. The artifacts are open-sourced for community use, so other teams can inspect the proofs and reuse the framework. We explained the science of predicting AI misbehavior in October, and verification is the other half of that problem: proving what code does, rather than predicting what it might do. If agents can prove a protocol correct in four weeks, the question for every lab shipping security-critical code is no longer whether formal verification is possible, but whether skipping it is still defensible.
By ByteHerald Staff. Google DeepMind reported on November 10, 2026, that its AlphaProof Code framework formally verified key security properties of the compiled code behind the Signal protocol, with agents powered by Gemini Carbon generating more than six million lines of Lean in four weeks, and that it is the first time the implementation of a widely deployed protocol has been formally verified by any method. The technical paper published with the announcement puts the target at libsignal version 0.105.4 with SPQR version 1.6.0, lists ten symbolic theorems covering forward secrecy, post-compromise security, authentication, and handshake secrecy, and counts 6.5 million lines of Lean including comments and blank lines. The Register reported that the work covered Signal's post-quantum PQXDH handshake and Triple Ratchet, along with forward secrecy, authentication, post-compromise security, and handshake secrecy. WIRED reported that DeepMind did the Signal analysis free of charge as a research project, that Google declined to share what it cost, and that the company would not say whether a commercial verification product is coming.
Comments
Post a Comment