DeepMind's AI Agents Wrote 6.5 Million Lines of Proof About Signal's Code
Google DeepMind said in a technical report dated Nov. 10, 2026, that teams of AI agents generated about 6.5 million lines of machine-checked proof that the compiled code of libsignal, the reference implementation of the Signal messaging protocol, meets a written set of security properties.
Formal verification, which proves mathematically that a program does what its specification says, has been too slow and costly for most software. The report notes that the formally verified seL4 microkernel took twenty person-years, and says the Signal proof work was done by a team of five over four weeks. The report says Signal's protocol protects the communications of billions of people, with variants of it running in WhatsApp, Meta's Messenger and Google Messages.
According to the report, the proofs cover the PQXDH handshake that opens a conversation and the Triple Ratchet that gives each message its own key, and they establish properties including forward secrecy, which keeps earlier messages unreadable if a key leaks later. The team compiled the unmodified libsignal code with the standard Rust compiler and stated its theorems about the resulting executable, so the proofs are about the binary rather than a model of the protocol or a rewritten version of the code.
The authors call these "the first proofs connecting protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation." No independent evaluation of the work has been published. The proofs also rest on about 26,000 lines of specifications and machine semantics the team wrote and approved itself, so the result covers what those specifications state, on one processor architecture and for one-to-one conversations.
The report says none of the authors wrote any proof code, and that a gatekeeper step accepts a proof only once the Lean proof assistant rechecks it against a held-out copy of the specification. To test whether the specifications were strong enough, the team reintroduced bugs previously found and fixed in libsignal and proved that the rebuilt binaries break its security theorem. Google DeepMind says it is open-sourcing all of the Lean specifications and proofs.
