DeepMind's AI agents formally prove chunks of Signal in four weeks

Four weeks for a proof of concept

According to a WIRED story republished on 11 November 2026 by Ars Technica, researchers at Google DeepMind used AI agents to formally verify, meaning mathematically prove, several of the Signal protocol’s key cryptographic guarantees. The project, billed as a proof of concept, took four weeks and runs on a new in-house framework called AlphaProof Code.

The stakes are not small. This protocol protects conversations in the Signal app, but also in Google Messages and WhatsApp. In other words, a considerable share of the planet’s chats, including the one where you swore you’d look at that ticket tomorrow.

What the AI actually changes

Formal verification is the old holy grail of software security: instead of testing a program and hoping you trip over the bug, you demonstrate with mathematics that it does what it is supposed to do. The catch, until now, was human time. You had to describe the properties to prove, translate them into formulas, then build the proof. According to the article, it is mostly that last step the agents shorten considerably.

The result comes in two parts. On the portions examined, the analysis turned up no new vulnerabilities. And when the researchers fed AlphaProof Code old versions of Signal, carrying known flaws fixed long ago, the tool correctly identified them and showed that the protocol could not be formally verified there. A proof tool that knows how to say no is the only kind worth having. The specification and the proof have been published so others can build on them.

Over at Signal, chief technology officer Ehren Kret notes in a statement that previous verification efforts covered smaller portions of code, and that this approach lets them be extended considerably.

What is still out of reach

The caveats come from the researchers themselves. Scope first: the Signal mobile app has not been verified as a whole, only parts of the protocol. Then speed: DeepMind acknowledges it got a head start from the formal verification work the Signal Foundation had already done. Four weeks, then, but not four weeks from a standing start.

That leaves the question the whole industry is asking: does it scale, and at what price? The analysis was done for free, as a research project, and Google declined to say what it cost. The company would not say whether a commercial product or service is planned, either. Swarat Chaudhuri, a researcher at DeepMind, says he is very enthusiastic but concedes there is a long road ahead before the method can be applied to all the world’s software.

The human stays in the loop, on purpose

Pushmeet Kohli, DeepMind’s vice president of research, already pictures banks and other companies able to prove the properties of their code rather than cross their fingers. The dream is familiar. The invoice has yet to show up.

Above all, the team stresses its method, which Swarat Chaudhuri describes as a “human-AI collaboration process”: the agents contribute and correct themselves at nearly every step, but ask for human review at key moments. The researcher says he wants to avoid a world where AI sets the goals, writes the proofs and, in short, sits exams it wrote itself.

Any developer who has written their own tests at ten to five on a Friday knows exactly what he means. You can sweet-talk a test suite into a green tick. A formal proof doesn’t take bribes.