DeepMind Formally Verifies Signal's Crypto Protocol With 6.5M Lines of Proof

What happened

DeepMind introduced AlphaProof Code in its official blog on Nov 10: a multi-LLM agentic framework that combines human expertise in formal verification with AI agents, and whose target is the actual compiled code of Signal's libsignal crypto protocol rather than its design documents. DeepMind says this is the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been formally verified by any method.

The verification covers libsignal v0.105.4 and SPQR v1.6.0, compiled with stock rustc into a single AArch64 Linux executable and run in a command-line harness; it covers the post-quantum PQXDH handshake and the Triple Ratchet, proving forward secrecy, post-compromise security, initiator and responder secrecy, authentication and handshake secrecy across 10 symbolic theorems. It covers one-to-one sessions only, not group chats, servers, key generation or phone operating systems, and the underlying crypto primitives are assumed sound rather than proved.

The agents, powered by Gemini Carbon, wrote about 6.5 million lines of machine-checked Lean proof in four weeks (the blog body says over six million), work that historically took expert teams years; about 1% of the code was flagged for human re-review after the agents' audit pass, with the rest checked by Lean's kernel, and the trusted base is about 26,000 lines. As validation, two previously fixed libsignal bugs were reintroduced into an isolated copy, and the system twice produced a machine-checked proof that the buggy version was insecure. The artifacts are open-sourced and a technical paper is published; Signal CTO Ehren Kret calls the work a major breakthrough in the DeepMind blog.

Key facts

1. System: AlphaProof Code, a multi-LLM agentic framework combining human expertise with AI agents, verifying compiled code rather than design documents
2. Target: libsignal v0.105.4 and SPQR v1.6.0, compiled with stock rustc into a single AArch64 executable; covering the post-quantum PQXDH handshake and Triple Ratchet
3. Scale: About 6.5 million lines of machine-checked Lean proof, completed in four weeks; comparable work historically took expert teams years
4. Review: About 1% of the code was flagged for human re-review after the agents' audit pass, the rest checked by Lean's kernel; the trusted base is about 26,000 lines
5. Validation: Two previously fixed libsignal bugs were reintroduced into an isolated copy; in both cases the system produced a machine-checked proof that the buggy version was insecure
6. Scope: One-to-one sessions only; no group chats, servers, key generation or phone operating systems; the underlying crypto primitives are assumed sound, not proved