Google DeepMind uses AI agents to formally verify Signal’s core code

What is changing?

Google DeepMind introduced AlphaProof Code, a framework that combines multi-model agents with human expertise. Researchers translated Signal’s security goals into formal mathematical specifications, while Gemini Carbon-powered agents generated more than six million lines of Lean. Lean machine-checked every proof, and human experts performed a second review of roughly one percent of the code flagged by the agents.

Rather than stopping at protocol design, the team says it proved in four weeks that the compiled core code satisfies the specified security properties. The system also produced machine-checked proofs of insecurity when two previously fixed real bugs were reintroduced into isolated versions. DeepMind said it is open-sourcing the formal-verification artifacts for community use.