DeepMind's AI proved that Signal's encryption code keeps its key security promises

Google DeepMind says its AI agents have mathematically proven that the code behind Signal's encryption for one-to-one chats delivers its main security promises. The work, announced on November 10, used a new framework called AlphaProof Code and checked the compiled program itself, the code that actually runs. According to DeepMind, this is the first time the implementation of a widely deployed cryptographic protocol has been formally verified by any method, with or without AI. The proof found no new flaws in the parts it covered.

What exactly was proven

Formal verification means writing down a security property as a mathematical statement and proving that the program always satisfies it, instead of testing it on examples. Most work on protocols like Signal stops at the design. DeepMind went down to the machine code: the team took libsignal version 0.105.4 and the spqr library, compiled them for 64-bit ARM Linux with the standard Rust compiler and reasoned about the resulting executable, the technical write-up says.

Researchers and several AI models first turned Signal's security goals into formal specifications, and humans reviewed every one. Then agents running on Gemini Carbon wrote the proofs in Lean, a language whose checker confirms every step automatically. The result is about 6.5 million lines of proof. The agents flagged roughly 1% of it for human review, and the whole project took four weeks. Among the ten proven theorems are forward secrecy, which keeps past messages safe if a key leaks later, and post-compromise security, which restores protection after a device has been temporarily hacked.

To check that the system can tell good code from bad, the team put two real, long-fixed Signal bugs back into an isolated copy of the code. In both cases AlphaProof Code produced a machine-checked proof that the buggy version was insecure.

What stays outside the proof

The write-up lists the limits in detail. The mobile apps were not verified directly, and the authors only expect the results to carry over if the apps run the protocol code unchanged. Group messaging is left for future work. Side channels, such as leaks through timing or power use, are out of scope, as are key generation and use across several devices. The proofs also assume that the underlying cryptographic building blocks are sound. Signal's chief technology officer Ehren Kret said the work "gives us even greater confidence" in the code's privacy guarantees.

DeepMind's blog names Signal and Google Messages as apps protected by the protocol. WhatsApp adopted the Signal protocol years ago, but the proof covered Signal's own libsignal code, not WhatsApp's software, so it says nothing new about WhatsApp. The work partly built on earlier formal verification of Signal done without AI. The method is also expensive: Google told Wired the approach is computationally demanding, and research scientist Swarat Chaudhuri said there is "a long distance to go before we are able to scale this to all the software of the world," 9to5Mac reports. DeepMind has published the proofs on GitHub, so outside experts can check them.