Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
Source
deepmind.google
Date
Why it matters
Agents paired with human experts proved security properties of real Signal protocol code, not a model of it. That shows agentic formal verification can now reach deployed cryptographic software.
Key takeaways · AI-distilled
Humans wrote the specs, agents wrote the proofs: researchers worked with several models to turn Signal's security goals into formal specifications, reviewed each one, then Gemini Carbon agents generated over six million lines of Lean proof.
The proofs cover the compiled implementation, not just the protocol design. DeepMind says most protocol verification stops at design level, while real vulnerabilities often hide in the gap between design and code.
Agents audited their own proof and flagged about 1% of the codebase for human review; Lean machine-checks the rest, so experts spent their time only where judgment was needed.
As a sanity check, the team reinserted two real, previously fixed Signal bugs into an isolated copy, and the system produced machine-checked proofs that both buggy versions were insecure.
DeepMind reports the verification took four weeks versus the years such work historically takes expert teams, and says it is open-sourcing the formal verification artifacts.
Terms in this piece · Glossary
LLM — A large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.
articleClaude Formally Verifies 123 Open-Source Libraries at the Binary LevelAnthropicAI
articleMAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic OutputsAlbert Wu, Nicholas Roberts, Tzu-Heng Huang, Haoran Lin, Gil Friedman, Sungjun Cho, Gabriel Orlanski, Frederic Sala
videoYour Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWSAI Engineer