Google DeepMind’s AI agents mathematically prove key security protections in the code behind Signal’s encrypted messaging

Google DeepMind, Google’s AI research lab, said Nov. 10 that teams of its AI agents produced a mathematical proof, checked by computer, that the actual code behind the Signal protocol delivers key security protections.  The Signal protocol scrambles messages so only the sender and recipient can read them.  It runs in the Signal app, and versions of it protect chats in WhatsApp, Meta’s Messenger and Google Messages, the researchers wrote.

DeepMind says it is the first time the code of a widely used encryption protocol has been verified this way, by any method.  That matters because many real attacks slip through gaps between a security design on paper and the code that runs on phones.  “Using AI agents to translate live code into valid Lean theorems is a major breakthrough,” said Ehren Kret, Signal’s chief technology officer.

What was proved

• Forward secrecy:  someone who steals a phone’s current keys still can’t read earlier messages.
• Post-compromise security:  after a break-in, the conversation locks the intruder out again once the two phones exchange fresh keys, as long as the intruder only listens.
• Authentication:  you are talking with the person you think you are.
• Handshake secrecy:  the secret two phones agree on when a chat starts stays hidden, in one of the two proofs even from a future quantum computer.

To test the system, the researchers put back two real bugs that had been found and fixed in Signal’s code.  In both cases it produced a proof that the buggy version was insecure.

How it works

Formal verification means proving with mathematical logic that software always does what it should, instead of testing it on examples.  It is the strongest security check there is, but it has been so slow that it is rarely used.  Verifying the seL4 operating-system kernel, one of the field’s best-known successes, took 20 person-years, the paper notes.

In AlphaProof Code, people work with AI to write a precise statement of what the code must guarantee, and human experts approve it.  Then teams of 40 to 80 AI agents, built on Google’s Gemini models, write the proof in Lean, a programming language that checks every step of a proof automatically.  The proofs total about 6.5 million lines.  Because Lean rejects any faulty step, people don’t have to trust the agents.  They only need to check about 26,000 lines of specifications and rules describing the chip.  The agents worked on the compiled machine code for the ARM-style chips used in nearly all Android phones and all iPhones.

Limits

The proofs assume the underlying encryption math is secure, and they cover one-on-one chats, not group chats.  They were done on a research build of Signal’s code library run as a simple command-line program, not on Signal’s phone apps, though the apps run the same code, the researchers wrote.  The second proof, which measures how hard the protocol is to break, does not cover quantum attackers.  DeepMind has published its proofs for others to check.

Sources:  Google DeepMind blog post, Nov. 10, 2026; AlphaProof Code technical paper; proof code on GitHub; Signal:  Quantum Resistance and the Signal Protocol; Lean programming language.