About 6.5 million lines of Lean proof, written by AI agents, establish key security properties of the actual machine code of libsignal, the Signal protocol's reference implementation. Google DeepMind announced it on November 10, 2026, under the name AlphaProof Code. The striking part isn't the size of the proof but how little of it you have to trust: roughly 26,000 lines.
What was proved
The team compiled libsignal's unmodified Rust code with the stock rustc compiler to AArch64 Linux machine code, then loaded that executable into Lean alongside a formal semantics of the architecture. Against that binary, the agents proved the properties Signal is supposed to deliver in its two core components, the post-quantum PQXDH handshake and the Triple Ratchet:
| Item | Value |
|---|---|
| Agent-generated proofs | ~6.5 million lines of Lean |
| Trusted base | ~18,000 lines of specification + ~8,000 of AArch64 semantics |
| Properties | Forward secrecy, authentication, post-compromise security and handshake secrecy |
| Time | Four weeks |
| Human review of proofs | About 1% of the code, flagged by the agents themselves |
To check that the specification catches real mistakes, they reintroduced two previously fixed libsignal bugs into an isolated copy. In both cases the system produced a machine-checked proof that the resulting binary violates the security theorems.
How it works
AlphaProof Code splits the work the way a research team would. A writer agent, guided by human experts, turns models and properties from the academic literature into a Lean specification; reviewer agents critique it and a person signs off. A team of prover agents powered by Gemini Carbon then proves that the executable meets that specification. A "gatekeeper" agent only accepts a proof if Lean's kernel checks it and it proves exactly a held-out copy of the specification, so no agent can quietly weaken what's being proved.
Why it matters
Most formal verification of protocols stops at the design. Earlier analyses of Signal looked at the handshake and the ratchet separately, and predate the post-quantum ratchet. Here the guarantee reaches the code that actually runs, which is where real vulnerabilities tend to hide: in the gap between what the design says and what the implementation does.
The paper sums up the deeper shift itself: the bottleneck in formal verification is no longer writing proofs, it's writing the specification. Nobody needs to read a multi-million-line proof, because Lean rejects it if it contains a logical error. What does need review is whether the specification says what you think it says. For anyone building critical systems, that moves expert effort from proving to specifying, and opens the door to verifying code that wasn't worth the cost until now: DeepMind names medical device firmware and power grid software as the next candidates.
For the wider industry, it's also a commercial argument. Google pitches formal verification as a complement to defensive agents like CodeMender against AI-driven threats, and Signal, through its CTO Ehren Kret, backs the approach.
What we don't know yet
DeepMind is publishing the Lean specifications and proofs, but not AlphaProof Code as a tool, nor the compute cost of those four weeks. The guarantee also depends on what sits outside it: the cryptographic primitives are assumed secure through contracts, and the result covers the AArch64 binary, not every build on every platform. The team itself says scaling the approach "requires continued research".
Sources
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Google DeepMind, November 10, 2026.
- AlphaProof Code: Verifying Signal's Security at the Machine-Code Level, technical paper and Lean development, Google DeepMind.
- Hacker News discussion, November 10, 2026.