DeepMind Mathematically Proves Signal Code Security in 4 Weeks Instead of Years

Anyone who has written cryptography knows an unpleasant truth: a protocol can be elegantly proven on paper, and a vulnerability will still turn up in the code. There is a chasm between the scheme and its implementation, and that is where real bugs live. Google DeepMind says it has taught AI agents to bridge that chasm for one of the most important protocols in the world, the one that protects conversations in Signal and Google Messages.

What exactly was done

The system is called AlphaProof Code. It is a multi-agent framework built on several LLMs that divides the work the way a research team would. First, human experts together with models translate Signal's security goals into formal mathematical specifications. Each specification is checked manually by a human. Then agents running on Gemini Carbon write the proofs themselves in the Lean language, producing more than six million lines.

Next comes the most practical part. Lean itself checks the correctness of every proof, so there is no need to trust the model blindly: an incorrect conclusion simply will not pass verification. The agents also additionally audited the result and flagged places that need a human's eye. That is about 1% of the codebase. Experts focused on those places rather than rereading millions of lines.

Why this is not just another audit

Ordinary formal verification of protocols stops at the design level: it proves that the scheme is secure. Here the agents went further and proved properties for the compiled code that runs on devices. For example, that messages remain protected before and after a temporary compromise of a device.

To test the system's honesty, the authors ran a simple experiment. They reintroduced two real, previously fixed bugs into an isolated version of the Signal code. In both cases, the system produced a machine-checkable proof that this version is insecure. In other words, the tool distinguishes correct code from incorrect code rather than simply "approving" everything.

According to DeepMind, the whole effort took four weeks, whereas for teams of experts such work has traditionally taken years. Signal's CTO Eren Kret called the automatic translation of production code into Lean theorems a major breakthrough.

Limitations and practical takeaways

It is worth keeping the scale in perspective. This is a single protocol that has long been studied thoroughly, and most of the stated figures rely on DeepMind's self-reporting. Humans have not been removed from the process: what counts as "secure" is still specified by experts, and an error in the specification yields a proof of the wrong thing. The authors themselves say that further research is needed to scale this up. The stated directions, medical device firmware and power grid software, are so far only plans.

What does this mean for developers and founders?

• The pairing of "an LLM writes, a formal checker accepts or rejects" is a workable scheme for tasks where the cost of error is high. The model is allowed to be wrong; the checker is not.
• If you build cryptography, payment logic, or critical embedded code, formal verification is no longer the preserve of academic teams with multi-year budgets.
• The skill of formulating specifications becomes more valuable than the skill of writing proofs. The bottleneck shifts to the question "what do we actually want to guarantee?"

An added plus is that DeepMind is opening up the verification artifacts. They can be studied and used as a template for your own experiments with Lean and agents. Together with tools like CodeMender, which find and fix vulnerabilities, formal proofs become part of the ordinary defensive perimeter rather than a rare academic curiosity.