Google DeepMind said its AI agents have mathematically proven key security properties of the code behind the Signal protocol. The protocol protects private messages in apps such as Signal and Google Messages.
The company said this is the first time AI has formally verified a widely deployed cryptographic protocol at this depth. It is also the first time the implementation of such a protocol has been formally verified by any method, with or without AI.
The work used a new system called AlphaProof Code. Google DeepMind, the AI research lab owned by Alphabet, described it as an agentic framework that pairs human experts with AI agents.
Humans Set the Rules, Agents Did the Proofs
Formal verification means using math to prove that code runs correctly without flaws. It is considered the highest standard of security assurance, but it is hard and often takes a lot of manual work.
AlphaProof Code splits the job the way a research team would. Human experts work with AI to decide what needs to be proven, and a group of AI agents carries out the proofs.
First, researchers worked with several AI models to turn Signal’s security goals into formal mathematical specifications. Human experts reviewed every specification before it was used.
Agents powered by Gemini Carbon then wrote the proofs. They produced more than six million lines of Lean, a computer language used to mathematically prove that code is accurate.
The agents also audited their own proofs and flagged areas that needed a human check. Those areas made up about 1% of the codebase, and Lean automatically checked the rest.
Four Weeks Instead of Years
Most protocol verification stops at the design level. DeepMind said its agents went further, proving that the compiled code running on devices delivers key security properties.
One of those properties is keeping messages protected before and after a device is temporarily compromised. Real-world flaws often hide in the gap between a design and the code that puts it into practice.
The full verification process took four weeks. According to DeepMind, the same type of task has historically taken teams of experts years.
To check that the system can tell good code from bad code, researchers put two real bugs back into an isolated copy of Signal’s code. Both bugs had been fixed in the past.
In both cases, AlphaProof Code produced a machine-checked proof showing the buggy version was insecure. Every proof in the project, including these, was checked by Lean.
Signal Chief Technology Officer Ehren Kret said earlier formal verification work focused on smaller portions of code. “Using AI agents to translate live code into valid Lean theorems is a major breakthrough,” he said.
Kret added that rigorously verifying the protocol gives Signal greater confidence in its code’s privacy guarantees. He said this matters as AI-driven security threats grow.
DeepMind said formal verification can work alongside automated defense agents such as its CodeMender tool. The company also said scaling these techniques will require more research.
Google DeepMind is open-sourcing its formal verification artifacts for public use. It has also released a technical paper describing the method.
