DeepMind used AI to formally prove key Signal guarantees in 4 weeks

Tests show that code works on the cases you thought to check. Formal verification answers a different question: can you mathematically prove that code will not violate a given property for any possible input? For security this is a long-standing dream, but in practice it runs into cost. Now it has a notable new argument in its favor: Google DeepMind used AI agents to prove key guarantees of Signal's cryptographic protocol.

What exactly was done

The DeepMind team used a new framework called AlphaProof Code. The work took four weeks and was conceived as a proof of concept. The Signal protocol protects conversations not only in the Signal messenger itself, but also in Google Messages and WhatsApp, which makes it one of the most widely used cryptographic protocols in the world.

In simple terms, verification consists of three steps. First, people describe which properties the code must have. Then that description is translated into formulas. Finally, a proof is built showing that the code matches those formulas. Before the AI era, all three steps consumed months of specialists' work. According to the researchers, agentic AI sharply shortens the last step, the most labor-intensive one.

The system found no new vulnerabilities in the verified parts of the protocol. But the reverse was also tested: on old versions of Signal with long-fixed bugs, AlphaProof Code correctly showed that a proof could not be built. For practitioners this is an important signal. The tool does not rubber-stamp "everything is secure"; it really does stumble on genuine defects.

Where the catch is

It is worth assessing the scale soberly. The analysis did not cover the entire Signal mobile app, only individual parts of the protocol. Moreover, DeepMind did not start from scratch: Signal Foundation had previously carried out formal verification of smaller pieces of code. That gave the team a head start. Signal CTO Eren Kret notes that DeepMind's approach makes it possible to significantly expand coverage.

The industry's main question is scale and cost. DeepMind carried out the analysis free of charge as a research project, and Google declined to say how much it cost. Asked whether the company plans a commercial product or service for formal verification, it also gave no answer. Researcher Swarat Chaudhuri himself admits there is "still a long way to go" before this scales to all the world's software.

The human stays in the loop

The most interesting part is the process the team calls "human-AI collaboration." The agents contribute at almost every stage and fix their own mistakes, but at key decision points they ask for human review. Chaudhuri says outright that he does not want a "vibe world" in which AI formulates the goals itself, writes the proofs itself and essentially hands in tests to itself. A middle ground is needed.

The logic is clear. If a model both decides what needs to be proved and proves it, an error in the formulation of the goal will go unnoticed. The proof will be formally correct but will verify the wrong thing. That is why the specification of properties must be approved by a human who understands it.

What to do with this

Developers and founders whose products rely on critical logic (payments, cryptography, sync protocols) should start looking at formal verification as a real option rather than an academic curiosity. Since its cost is still unknown, it is too early to put it in a budget. But there is a concrete benefit: DeepMind is publishing the specification and proof for Signal, and they can be studied and used in other verification work.

According to Pushmeet Kohli of Google Cloud and DeepMind, banks and other companies that depend on correctness guarantees will be able to say, "I can prove these properties." For now that is more a promise than a finished product. But AI verification has passed its first serious test, on a real and massively used protocol.