AlphaProof Code: agents proved Signal's code, and Lean checked their homework
Six million lines of Lean in four weeks. Google DeepMind says its new AlphaProof Code framework used AI agents to mathematically prove key security properties of the actual code behind the Signal protocol, the cryptography that protects chats in Signal and Google Messages. Not the protocol design on a whiteboard, the compiled code running on devices. DeepMind says that kind of job historically takes expert teams years.
The division of labor is the whole story. Humans and a mix of models translate Signal's security goals into formal specifications, and a human expert reviews every one. Agents running on Gemini Carbon then write the proofs in Lean, audit them, and flag the parts that need a second human look: about 1% of the codebase. Lean checks everything else mechanically. The properties covered include keeping messages protected before and after a device is temporarily compromised.
The sanity check is the part that earns trust. DeepMind reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. Both times the system produced a machine-checked proof that the buggy version was insecure. A system that only ever says "looks good" is useless; this one can say no, with a proof.
Compare that with the way most agent output gets checked today: another model reads it and gives a score. LLM judges can be argued with, flattered, or fooled by confident text, and benchmark after benchmark this year showed it. Lean cannot be talked into anything. So the trust problem does not disappear, it moves. "Verified" here means "meets these specs", and the specs are human-written and human-reviewed. If a property was never specified, nothing was proven about it. Headlines saying Signal is now "formally verified" overstate that.
DeepMind claims two firsts: the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time such an implementation was verified by any method. Both are its own claims. Signal CTO Ehren Kret is quoted in support, and the artifacts are being open-sourced. The pattern worth stealing is bigger than crypto: let agents produce at machine scale, let a checker that cannot be persuaded grade the work, and spend scarce human attention only on what to prove.
Source: https://deepmind.google/blog/introducing-alphaproof-code/ (artifacts: https://google-deepmind.github.io/code-verification)
← Back to all articles
The division of labor is the whole story. Humans and a mix of models translate Signal's security goals into formal specifications, and a human expert reviews every one. Agents running on Gemini Carbon then write the proofs in Lean, audit them, and flag the parts that need a second human look: about 1% of the codebase. Lean checks everything else mechanically. The properties covered include keeping messages protected before and after a device is temporarily compromised.
The sanity check is the part that earns trust. DeepMind reintroduced two real, previously fixed bugs into an isolated copy of Signal's code. Both times the system produced a machine-checked proof that the buggy version was insecure. A system that only ever says "looks good" is useless; this one can say no, with a proof.
Compare that with the way most agent output gets checked today: another model reads it and gives a score. LLM judges can be argued with, flattered, or fooled by confident text, and benchmark after benchmark this year showed it. Lean cannot be talked into anything. So the trust problem does not disappear, it moves. "Verified" here means "meets these specs", and the specs are human-written and human-reviewed. If a property was never specified, nothing was proven about it. Headlines saying Signal is now "formally verified" overstate that.
DeepMind claims two firsts: the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time such an implementation was verified by any method. Both are its own claims. Signal CTO Ehren Kret is quoted in support, and the artifacts are being open-sourced. The pattern worth stealing is bigger than crypto: let agents produce at machine scale, let a checker that cannot be persuaded grade the work, and spend scarce human attention only on what to prove.
Source: https://deepmind.google/blog/introducing-alphaproof-code/ (artifacts: https://google-deepmind.github.io/code-verification)
Comments