Google DeepMind introduced AlphaProof Code yesterday, an agentic framework for formal verification, and used it to prove key security properties of the code behind the Signal protocol — the technology that protects conversations in Signal and Google Messages.
What is actually new here
Protocols like this have been formally analysed for decades, but almost always at the design level. DeepMind proved the implementation: that the compiled code fulfils the security properties, down to what actually runs on devices. That includes the guarantee that messages stay protected before and after a device is temporarily compromised.
By DeepMind’s own account that is a first twice over. It is the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time the implementation of such a protocol has been formally verified by any method at all. Real-world vulnerabilities usually hide exactly where design and implementation drift apart.
How the work was split
AlphaProof Code is a multi-model framework that divides verification the way a research team would. First, researchers worked with a mix of models to translate Signal’s security goals into formal specifications, with human experts reviewing every one. Then agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean.
The agents then audited the proof themselves and flagged what a human should look at: one percent of the codebase. Lean checks the rest automatically. The whole process took four weeks, a job that has historically taken expert teams years.
As a control, the researchers reintroduced two real, previously fixed bugs into an isolated version of Signal’s code. The system caught both.
Two swarms, two aims
Two days ago this site covered a thousand Claude agents formalising Fermat’s Last Theorem in Lean in 28.7 hours. Now the same shape of setup arrives from Google, in the same proof language, aimed at software running on billions of devices.
The difference worth noticing is where the human sits. At Anthropic the mathematics was the goal and the agent count was the method. At DeepMind humans stay at the centre of the specification: experts decide what gets proved, and every specification is signed off by hand. Proving is then the assembly line. For security work that is the saner split — a proof of the wrong property is not progress, it is a well-documented mistake.