Google DeepMind uses AI agents to formally verify Signal messaging security

Google DeepMind researchers have completed a formal verification of Signal's messaging protocol using AlphaProof Code, a multi-agent framework designed to mathematically validate software. The system verified the app's post-quantum PQXDH handshake and Triple Ratchet implementation, confirming the cryptographic design behind libsignal's forward secrecy, authentication, handshake secrecy, and post-compromise security. [2][3]

The framework translates security properties into Lean specifications before Gemini Carbon agents generate proofs. For this project, the agents authored 6.5 million lines of Lean code, which were checked by the Lean kernel and flagged for human auditing. DeepMind notes the proof is theoretical because it assumes perfect cryptography and does not guarantee the computational secrecy of raw bytes. The effort required four weeks of work by a five-person team alongside substantial computing tokens. [2]

Researchers claim this marks the first time artificial intelligence has helped connect protocol-level security guarantees directly to a widely used cryptographic implementation. While past software verification milestones like the seL4 microkernel took 20 person-years, DeepMind hopes expanding such automated specification and verification techniques can protect broader software ecosystems against emerging offensive AI threats. [2][3]