DeepMind formally verified key guarantees of the Signal protocol in four weeks

Tests show that code works on the inputs you thought to check. Formal verification answers a different question: can you mathematically prove that the code behaves correctly on any input. Engineers have long called this the holy grail of security, but in practice proofs were written by hand, and that took months or years. Now DeepMind has shown that a significant part of this work can be handed off to an agent.

What exactly was done

Researchers at Google DeepMind used a new framework, AlphaProof Code, to formally verify a number of key cryptographic guarantees of the Signal protocol. This protocol underpins encryption in the Signal app, Google Messages and WhatsApp. The project was a proof of concept and took just four weeks.

To appreciate the speed, you need to understand what the work consists of. First, people describe what properties the code should have. Then that description is turned into formulas. And only after that is the proof itself written. Agentic AI significantly cuts the time at precisely this last, most labor-intensive stage.

There was also a practical check. The system found no new vulnerabilities in the parts of the protocol it examined. But on older versions of Signal with long-fixed bugs, AlphaProof Code found those problems and showed that such code cannot be formally verified. For a verification tool this is an important test: it does not simply confirm that "everything is fine" but genuinely fails where the code is wrong.

The researchers did not start from scratch. Signal Foundation had previously done formal verification of smaller code fragments, and that gave DeepMind a head start. Signal's chief technology officer Eren Kret says DeepMind's approach allows the coverage of verification to be expanded noticeably, and this adds confidence in the privacy of the implementation.

Why this matters for practitioners

The main shift here is cost. Formal verification was out of reach for most teams not because no one understood its benefits, but because proofs were too expensive in human time. If agents take over the routine work, the range of code worth proving expands. Pushmeet Kohli of Google Cloud and DeepMind speaks directly about banks and other companies that will be able to say: "I can prove these properties."

The most sensible thing about the project is how the work is organized. Agents contribute and self-correct at almost every step, but at key points they request human review. DeepMind researcher Swarat Chaudhuri explains why: what is needed is not a "vibe world" in which the AI generates the goals itself, writes the proofs itself and essentially passes tests it wrote itself. What is needed is a happy medium.

For a developer, a simple takeaway follows. A proof is valuable only to the extent that the specification is correct, that is, the description of what counts as correct behavior. If a model writes both the specification and the proof, you get a pretty piece of paper with no guarantees. Responsibility for formulating the requirements remains with the human.

Limitations and what to do

It is worth taking a sober view of the scale. The whole Signal mobile app was not verified, only individual parts of the protocol. Chaudhuri himself admits that verifying all the software in the world is still very far off. The system found no new bugs, so for now this is more a confirmation of other people's work than a discovery.

The industry's main question is economics. DeepMind did the analysis for free as a research project, and Google has not disclosed the cost. The company also declined to comment on a commercial product or a formal verification service. In other words, there is no ready-made "verify my code" button yet.

What you can do right now. The researchers are publishing the specification and proof for Signal, and it is good learning material for those who write critical code: payments, cryptography, trust infrastructure. If you work in such areas, it makes sense to follow how tools like AlphaProof Code evolve from a demonstration into a product, and to learn in advance to formulate code properties so that they can be proved. It is this skill, rather than the ability to write proofs by hand, that will apparently become valuable.