Google DeepMind uses AI agents to formally verify Signal's protocol code

Human experts worked with a mix of models to translate Signal's security goals into formal mathematical specifications, and reviewed each one. Agents powered by Gemini Carbon then wrote the proofs in Lean, generating more than six million lines of code.

The agents audited their own proofs and flagged about one percent of the codebase for a second look by a human reviewer, while Lean checked the rest automatically. The proofs cover the compiled code running on devices, not only the design, which Google DeepMind says is where real-world vulnerabilities often hide.

To test the system, the researchers reintroduced two previously fixed bugs into an isolated version of Signal's code. In both cases, AlphaProof Code produced a machine-checked proof that the buggy version was insecure. Google DeepMind says it is open-sourcing the formal verification artifacts.

Teams building agents that handle cryptography or other security-critical code now have a worked example of pairing human-written specifications with agents that produce Lean proofs. The work shows that checks at the design level alone can miss implementation bugs, so verification of the actual code is worth considering. The open-sourced artifacts give developers something concrete to inspect and reuse.