AlphaProof Code
Google DeepMind introduced AlphaProof Code, an agentic framework that formally verified the code of Signal's cryptographic protocol in Lean in four weeks.
AlphaProof Code is a multi-LLM agentic framework where human experts and AI decide what to prove, and agents powered by Gemini Carbon write the proofs in Lean, over six million lines. Agents then flagged about one percent of the codebase for human review, and Lean checks the rest. DeepMind says it is the first formal verification of a widely deployed cryptographic protocol's implementation at this depth, by any method.
- Date
- Tuesday 10 November 2026
- Lab
- Google DeepMind
- Kind
- product
- Access
- paper only
Figures
| Measure | Value | Measured by |
|---|---|---|
| Lines of Lean proof generated | over six million the item summary said three million; the blog page says over six million | company |
| Share of codebase flagged for human review | 1% | company |
| Verification time | four weeks DeepMind says this historically takes expert teams years | company |
| Reintroduced real bugs detected | 2 of 2 system produced machine-checked proofs that the buggy versions were insecure | company |
Verification artifacts are being open-sourced; the framework itself is not described as available to users.
Sources
This record was checked against its sources on 10 November 2026. How we check