Google DeepMind’s AI agents formally verify Signal’s encryption code

Google DeepMind says AI agents have mathematically proved that the code behind Signal’s encryption keeps its main security promises. The lab announced the result on 10 November, together with a new framework called AlphaProof Code and a technical paper.

The Signal protocol protects chats in the Signal app, WhatsApp, Messenger and Google Messages. DeepMind’s researchers checked libsignal, the open-source Signal encryption library, down to the machine code that runs on a device. The lab called this a first in a DeepMind blog post. Nobody had formally verified the code of such a widely used protocol before, “by any method, with or without AI”, it said. The technical paper sets out the method and its limits.

“As AI-driven security threats grow, having the core Signal protocol rigorously verified with automated theorem proving gives us even greater confidence that our code delivers on its privacy guarantees,” Ehren Kret, Signal’s chief technology officer, said in a statement published by DeepMind.

How the agents did it

Formal verification uses maths to prove that software does what it should. Instead of hunting for bugs one at a time, it rules out whole classes of them. It has long been slow and costly: the paper notes that verifying the seL4 microkernel took 20 person-years.

AlphaProof Code splits the job. Humans chose what to prove. AI agents helped turn Signal’s security goals into formal specifications, with human experts reviewing each one. Teams of 40 to 80 agents running on Gemini 4 Carbon then wrote the proofs. They used Lean, a language for machine-checked maths.

The agents produced about 6.5 million lines of proof in four weeks, for a team of five researchers. None of the authors wrote proof code, according to the paper. Agents running on Gemini 4 Carbon and Anthropic’s Claude Opus 5.5 drafted and reviewed the specifications.

The proofs cover Signal’s post-quantum handshake and its Triple Ratchet, which gives every message a fresh key. They show forward secrecy, which keeps old messages safe if someone later steals a phone’s keys. They also cover authentication and post-compromise security, the protocol’s ability to recover after a breach.

To test the method, the team put back two old libsignal bugs that Signal had already fixed. In both cases, the system proved that the buggy code was insecure. It found no new flaws in the parts it checked, Lily Hay Newman reported for Wired.

What it does not prove

The guarantees are narrower than “Signal is secure”. The paper covers one-to-one chats in the researchers’ own build of the library, not the Signal apps. The researchers left group messaging for future work and did not verify key generation. The proofs also assume that the low-level cryptographic routines work as specified.

Neither proof shows the post-quantum healing that Signal’s newest ratchet layer aims to add, the paper says. Cost is also an open question. Google declined to share what the project cost, or whether it plans a commercial verification product, Wired reported.

“We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that,” Swarat Chaudhuri, a DeepMind research scientist, told Wired.

Chaudhuri told The Register that the hard part is now deciding what to check, not the checking itself.

“We really believe that the next frontier is not going to be proof but specification,” Chaudhuri told The Register.

The work is a step towards Signal Shot. The Beneficial AI Foundation, Signal and the Lean FRO set that challenge in April, to verify the Signal protocol and app in Lean. DeepMind is releasing its specifications and proofs on GitHub so that others can check them. Google opened Gemini 4 Carbon to paying developers this week.