- Who
- Google DeepMind
- What
- formally verified key security properties of the code underlying the Signal protocol using AlphaProof Code
- When
What happened
Google DeepMind researchers used AlphaProof Code to formally verify key security properties of the compiled code underlying the Signal protocol. The multi-LLM framework generated more than six million lines of Lean proofs, which Lean checked automatically; human experts reviewed every specification and focused on one percent of the codebase flagged for a second look. The process took four weeks, and tests with two previously fixed bugs produced machine-checked proofs that the buggy versions were insecure.
Why it matters
The work follows verification from Signal’s design goals to compiled code and reports a four-week process, showing where human review fits alongside machine-checked proofs.
Read next
See the full storyGoogle DeepMind Formally Verifies Selected Signal Protocol GuaranteesReported by 5 sources
The story so far
Google DeepMind used AlphaProof Code to formally verify selected cryptographic guarantees in the compiled code underlying the Signal protocol. The four-week proof of concept generated more than six million lines of Lean proofs, which Lean checked automatically; human experts reviewed every specification and examined the roughly one percent of the codebase flagged for a second look. The work found no new vulnerabilities in the portions examined. Tests using two previously fixed bugs produced machine-checked proofs that the older, buggy versions were insecure. DeepMind is releasing its specification and proof to support further formal verification work.