Google DeepMind used AI to mathematically prove key parts of Signal's encryption

Google DeepMind says it has used an AI system to formally verify a number of the core security guarantees in the Signal protocol, the encryption scheme that protects chats in the Signal app and is also used by WhatsApp and Google Messages. The project took about four weeks.

What "formally verified" means

Most software is tested by running it and looking for things that break. Formal verification goes further. You write down, in precise mathematical terms, what the software is supposed to guarantee, then build a proof that it always does. If the proof holds, an entire class of bugs is ruled out, not just the ones a tester happened to try.

The catch has always been effort. Describing the software's behavior, turning that description into formulas and then constructing the proof could take specialists months or years, which is why the technique has mostly been reserved for small, critical pieces of code. DeepMind's new framework, AlphaProof Code, uses agentic AI to take on much of the proof-building work.

What DeepMind found

The analysis didn't turn up any new vulnerabilities in the parts of the protocol it examined. As a check on the method, the researchers also ran it against older versions of Signal that contained known bugs, long since fixed. It flagged those problems and showed that those versions could not be verified, a sign that it wasn't simply rubber-stamping whatever it was given.

DeepMind says it's releasing the specification and proof it developed so other researchers can build on them. The team also acknowledged a head start: the Signal Foundation had already done some formal verification work of its own. Signal's chief technology officer, Ehren Kret, said in a statement that earlier work had focused on smaller portions of the code and that DeepMind's approach allows a significant expansion of what can be checked.

The limits

This is a milestone, not a clean bill of health for everything on your phone. The work covered parts of the protocol, not the full Signal mobile app, and DeepMind researchers stressed that there's a long way to go before the approach can scale to software in general.

Cost is the other open question. DeepMind ran the Signal analysis for free as a research project, and Google declined to say what it cost. Whether AI-driven verification can become cheap enough for banks, governments and ordinary software teams to use routinely is what will decide whether this stays a showcase or becomes standard practice.

Why it matters

Security researchers have long called formal verification a holy grail, because it replaces "we couldn't find a bug" with "we proved this kind of bug can't exist." If AI can shrink the time and expertise it takes, the world's most sensitive code could start shipping with mathematical guarantees attached. The Signal protocol, already one of the most scrutinized pieces of cryptography in use, is the first big-name test case.