Google AI agents verified the core of Signal's encryption in four weeks

To test their system, Google DeepMind researchers sabotaged an isolated copy of Signal's code. They reintroduced two real vulnerabilities that were fixed in 2025. The first caused the library to wrongly save a session state containing a secret key. The second, a so-called small-subgroup bug, stemmed from a missing check on received X25519 keys, the mechanism used for key exchange. In both cases, the machine produced a proof, checked automatically, that the booby-trapped version violated the expected guarantees.

Google DeepMind unveiled the tool, AlphaProof Code, on November 10. The division of roles is simple: human experts decide what needs to be proven, and AI agents, powered by Google's Gemini Carbon model, write the proofs. They are written for Lean, a “proof assistant” that mechanically accepts or rejects each step. The first target: libsignal, the reference library for the Signal protocol. That protocol protects the messaging app of the same name and, according to DeepMind, Google Messages.

A proof about the program that actually runs

The work covers two-party conversations. It covers the initial key exchange, called PQXDH, which includes protection against quantum computers. It also covers the “Triple Ratchet,” which renews keys as messages are exchanged. The properties proven include:

• forward secrecy: a stolen key does not allow old messages to be read;
• post-compromise security: protection is restored after a temporary breach;
• authentication of the parties;
• in the so-called symbolic model, resistance to the “harvest now, decrypt later” strategy.

What is new is the level of the proof. It does not target the source code, but the program compiled for 64-bit ARM processors from the public, unmodified versions of libsignal (0.105.4) and its post-quantum module SPQR (1.6.0). There is therefore no need to trust the compiler. According to the technical paper, the agents produced about 6.5 million lines of proof. They rest on some 26,000 lines of specifications and processor description.

The project took a team of five people four weeks, according to The Register. The site reports that the research paper compares this timeframe with the 20 person-years that verifying the seL4 microkernel required. “Using AI agents to translate production code into valid Lean theorems is a major breakthrough,” says Ehren Kret, Signal's chief technology officer, quoted by DeepMind.

What the proof leaves out

The authors themselves list what is not covered:

• side-channel attacks, which observe computation time for example, and other secrets present in memory;
• group conversations, multi-device use, and the Android and iOS apps themselves;
• key generation and the code of the cryptographic building blocks (ML-KEM, Kyber, operations on the X25519 and Edwards curves, HMAC in the SPQR module), replaced by “contracts” assumed to be respected;
• the quantum attacker in the so-called computational proof, as well as SPQR's own post-quantum recovery.

In other words, the logic of the post-quantum exchange is verified, but the soundness of the algorithms themselves remains an assumption: the symbolic model assumes perfect cryptography. Swarat Chaudhuri, a DeepMind researcher, admits to The Register that the approach is not “the last word.” In his view, the difficulty shifts to the specifications, that is, deciding what to prove. According to DeepMind, the agents also flagged about 1% of the code for a second human look.

What this means for you

Signal users don't need to do anything. For companies, formal verification, long reserved for a few very expensive projects, could become feasible for critical cryptographic code. While OpenAI and Anthropic are funding, with the Simons Foundation, a program to help mathematicians verify results obtained with AI, DeepMind's proofs are checked by a machine. The proofs are published on GitHub. However, DeepMind has neither put a figure on the cost of the operation nor announced a commercial service. It remains to be seen whether the method can keep pace with Signal's updates, and whether it will work on much larger software.