Machine-checked proofs for Signal protocol code: scope, trust, and cost

Today Google DeepMind published something that has been a stated goal of the formal-methods community for years: machine-checked proofs that the actual compiled code of the Signal protocol delivers its security guarantees. I read the technical paper behind the announcement rather than just the blog, and the numbers there are worth having in one place, because most of the coverage stopped at the headline.

The framework is called AlphaProof Code, and the target is libsignal, the Rust reference implementation of the Signal protocol — the protocol that, in variants deployed in Signal, WhatsApp, Meta's Messenger and Google Messages, protects the messaging of billions of people. Earlier verification work proved things about protocol designs, or about reimplementations written to be easy to prove. This campaign proves theorems about an unmodified build: libsignal linked into a small command-line harness, compiled by the stock Rust compiler, verified as AArch64 machine code running under a formal semantics of the instruction set in the technical paper.

The numbers, checked at the paper: about 6.5 million lines of machine-checked Lean, of which 5.3 million cover the shared binary. The verified code itself is roughly 560 KB, about 140,000 AArch64 instructions. What a reader must actually trust is far smaller: about 18,000 lines of specification statements plus about 8,000 lines of machine semantics. The proof work was done by five people in four weeks, with proof generation handled entirely by agent teams — the authors state that none of them wrote proof code. For scale: verifying seL4 took about twenty person-years; CompCert about six.

The properties proved: forward secrecy, authentication, message confidentiality, post-compromise security, and secrecy of the post-quantum PQXDH handshake — the latter against a future quantum attacker in the symbolic model only. Two previously fixed libsignal bugs were reverse-applied and recompiled, and Lean then proved the buggy binaries violate the symbolic security theorem: the specs catch real mistakes, they are not vacuous.

What the proof does not cover, stated plainly, matters more than the headline. The low-level cryptographic primitives enter through contracts — assumed correct by specification, not verified here; the X25519 and Edwards curve operations are among those routines. The theorems are about one AArch64 Linux build of a command-line harness, not Signal's own apps; the authors argue they carry over to the Android and iOS builds only as long as those preserve the protocol code's behaviour. Only one-to-one sessions are covered; group messaging is left for future work. Lean's small kernel is trusted; the Rust compiler is explicitly not — a miscompile would break the theorem, which is the point of verifying at the machine-code level. The Lean development is public (google-deepmind/code-verification, a single initial commit 808b4b7 dated today, with the build scripts).

The result I found most durable is in the paper's least-celebrated section. Building the specifications against real code forced the team to catalogue every departure from the published literature, and some departures are outright errors in published analyses: fifteen gaps or bugs in the computational analysis of the Double Ratchet, printed ProVerif queries in Cheval, Jacomme and Richards' analysis that look up skipped message keys at the wrong ratchet index, a quantifier in the PQXDH analysis that makes its own corollary unprovable as written. DeepMind's agents and reviewers audited the security literature itself on the way to auditing the code, and found it wanting in places.

This is a response to the Beneficial AI Foundation's challenge from April to formally verify Signal with Lean — the paper calls its result a significant milestone towards that challenge; the app and group messaging stay open. The cost curve is the part to watch: if four weeks and five people is what machine-code-level assurance now costs for a protocol core, the argument that formal verification is only for the mission-critical few starts to collapse. The bottleneck, as one of the authors put it in The Register, is no longer proving — it is deciding precisely what to prove.