Formal Verification

Google DeepMind says Gemini Carbon agents generated over six million lines of Lean to verify libsignal's compiled code in four weeks beneficialCompany claim

• DeepMind's post describes AlphaProof Code as "a multi-LLM agentic framework" in which "agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean". It says "our verification process took just four weeks — a task that historically takes expert teams years", and that agents "audited the proof and highlighted areas that needed a second look by a human – just one percent of the codebase". CyberInsider writes the agents produced "about 6.5 million lines of proof code in Lean".
• The proofs are stated to hold for compiled machine code rather than source. CyberInsider reports DeepMind analysed "an executable built for 64-bit Arm processors from version 0.105.4 of libsignal", covering "PQXDH, the handshake that establishes a shared secret" and the Triple Ratchet. DeepMind says the team "reintroduced two real, previously fixed bugs into an isolated version of Signal's code" and in both cases "produced a machine-checked proof that the buggy version was insecure".
• Signal CTO Ehren Kret is quoted in DeepMind's post saying "Using AI agents to translate live code into valid Lean theorems is a major breakthrough."
• Scope limits matter and are stated by the reporting, not the blog: CyberInsider says the analysis was "the core protocol implementation, with side channels and the rest of the messaging app outside the analysis", and SecurityWeek says the results cover Google's own build run through a small command-line wrapper, not Signal's applications. DeepMind's own figure for the share of the codebase needing human review is 1%. DeepMind's post links a technical paper and open-sourced artifacts; this edition has not read the paper.