AlphaProof Code: AI agents verify Signal's real code

What happened?

Google DeepMind introduced AlphaProof Code on November 10 (Google DeepMind). It is a multi LLM agent framework for formal verification, the practice of mathematically proving that code runs correctly without flaws. Its first big result is the Signal protocol, which protects encrypted chats in Signal and Google Messages.

DeepMind says 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.

How it works

The work is split the way a research team would split it. Researchers worked with a mix of models to turn Signal's security goals into formal mathematical specifications, and human experts reviewed every one. Agents powered by Gemini Carbon then wrote the proofs, generating over six million lines of Lean, a language for machine checked proofs.

The agents then audited the proof and flagged the parts needing human attention, just one percent of the codebase. Lean checks the rest automatically, so experts could focus where human judgment matters most.

Why it matters

Most protocol verification stops at the design level. AlphaProof Code went further and proved that the compiled code meets key security properties, such as keeping messages protected before and after a device is temporarily compromised. Real world vulnerabilities often hide in the gap between design and implementation.

The whole process took four weeks, a task DeepMind says historically took expert teams years. As a sanity check, the team reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. In both cases the system produced a machine checked proof that the buggy version was insecure.

Signal CTO Ehren Kret said prior formal verification focused on smaller portions of the code, and called using AI agents to translate live code into valid Lean theorems a major breakthrough.

What it means for developers

This is an early sign that formal verification could leave the academic corner. If writing the spec stays human work and agents handle most of the proving, it becomes a realistic option for critical code. DeepMind is open sourcing the verification artifacts, and a technical paper is available.

Google wants to pair this with automated defense agents like CodeMender. The same research group recently used agents to find new weaknesses in RSA-1024, so DeepMind is working both the attack and the defense side.

What to watch

All numbers so far come from DeepMind itself, with no independent check yet. The released artifacts will be the first real test. DeepMind names medical device firmware and power grid software as next targets, but says scaling these techniques still needs more research.