DeepMind's AlphaProof Code Formally Verifies Signal Protocol

Google DeepMind unveiled AlphaProof Code (AlphaProof Code), which uses AI agents to mathematically prove the correctness of software, on the 10th (12:00 UTC). DeepMind said it used the system to verify the core code of the cryptographic protocol used by the Signal messenger in about four weeks, and claimed it was the first time an implementation of a widely deployed cryptographic protocol had been formally verified to this depth.

Formal verification has long been regarded as the most reliable method of software assurance. But because human experts had to write specifications in mathematical language and hand-craft the proofs connecting them to the code, it was used only in a handful of fields such as aviation and operating-system kernels. The Signal Protocol is a design for end-to-end encryption of conversations and is known to be used not only in the Signal app but in other messengers as well. Accordingly, bugs left in its implementation can have far-reaching consequences. The only basis for DeepMind’s “first” claim is what its blog presents, and there has been no independent confirmation yet.

Formal verification is a technique that shows, through mathematical proof, that a program behaves according to a given specification. Unlike testing, which tries only some inputs, a valid proof guarantees that the property holds in every case the specification covers. DeepMind checked the proofs with Lean, a proof assistant and language in which a computer mechanically checks each step of a proof; if a proof produced by an agent is wrong, it is caught at this stage.

The target of verification was the core security properties of the compiled code underlying the Signal Protocol. DeepMind said it proved that messages remain protected both before and after a point at which a device is temporarily compromised. In cryptography, these properties are called forward secrecy and post-compromise security, respectively. The blog claims this is the first formal verification of the protocol’s implementation — that is, the actual code.

Humans decide “what,” AI handles “how”

AlphaProof Code is an agent framework that combines multiple large language models (LLMs). The roles are divided: humans decide what to prove, and the AI agents produce the proofs themselves. Every proof is checked by Lean. Human involvement has been reduced but not eliminated. According to DeepMind, human experts review all formal specifications and re-examine about 1% of the codebase flagged by the agents. Because even a perfectly correct proof guarantees the wrong property if the specification is wrong, a structure in which humans remain responsible for the specifications to the end is a key safeguard of this approach.

The related post was written by DeepMind researchers Pushmeet Kohli and Swarat Chaudhuri, and Signal’s chief technology officer (CTO), Ehren Kret, was quoted in it.

DeepMind said the work took about four weeks and that the same task would previously have taken a team of experts years. As for the size of the Lean proofs, the body of the post says “more than 6 million lines,” while the page description says “more than 3 million lines,” so the two figures disagree. This article does not assert either.

A test was also disclosed. When two previously fixed bugs were reintroduced into an isolated copy of Signal’s code, the system produced a machine-checked proof that the buggy version was not secure. This can be read as a design meant to show that the proof system does not merely stamp code as “correct” but can also single out faulty code.

The scope of verification is Signal’s core cryptographic code and the specified security properties. It does not mean the entire Signal app has been verified, and the blog does not claim so. DeepMind wrote that further research is needed to extend the technology, and cited areas such as medical-device firmware and power-grid software as future targets.

Machine-checking of AI-generated proofs has been a recurring trend recently. One example is Anthropic’s earlier statement that more than 1,000 “Claude Fable 5.2” agents formalized Fermat’s Last Theorem in Lean in 30 hours (Anthropic’s own claim; see our report (in Korean)). The significance of this announcement is that the target has shifted from mathematical proofs to security software that is actually deployed.

Bugs in cryptographic software often pass code review and testing and persist for a long time. Formal verification is the strongest means of reducing them, but its high cost has confined it to a few projects. If, as DeepMind claims, agents can greatly cut the time and labor costs, verification of security-critical code could spread. However, all figures are DeepMind’s own announcements, and no third-party reproduction has been confirmed. Writing and reviewing specifications remains a human job.