TL;DR
What is Google DeepMind's AlphaProof Code?
Google DeepMind's AI agents proved that key security parts of Signal's encryption code work as designed. That's good news if you use Signal or Google Messages, and a sign that checking software this carefully is getting faster. There's nothing you need to do yet.
What did Google DeepMind announce?
On Tuesday, November 10, 2026, Google DeepMind introduced AlphaProof Code, a system where human experts and AI agents work together to "formally verify" software. Formal verification means mathematically proving that code behaves exactly as its specification says, instead of just running checks and hoping nothing slipped through.
The first big target was the Signal protocol, the encryption method that protects chats in the Signal app and in Google Messages. DeepMind says it's the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time the implementation of a protocol like this has been formally verified by any method.
How AlphaProof Code checked Signal's code
DeepMind splits the job the way a research team would:
- Humans decide what to prove. Researchers worked with several AI models to turn Signal's security goals into formal specifications, and human experts reviewed every one.
- Agents write the proofs. Agents running on Gemini Carbon wrote over six million lines of Lean, a programming language built for mathematical proofs, where every step gets checked by the computer.
- Humans check the hard spots. The agents flagged about 1% of the code for a second look by a person. Lean checks the rest automatically.
The proofs go all the way down to the compiled code that actually runs on devices, not only the design on paper. That matters because, as DeepMind puts it, "real-world vulnerabilities often hide in the gap between design and implementation." One of the properties proved is that messages stay protected before and after a device is temporarily compromised.
DeepMind says the whole job took four weeks, "a task that historically takes expert teams years." Read our story on how DeepMind's AI agents found two weak spots in 1024-bit RSA.
Did the AI catch real bugs?
As a check, the team put two real, already-fixed bugs back into an isolated copy of Signal's code. In both cases, AlphaProof Code produced a machine-checked proof that the buggy version was insecure. So the system can tell good code from broken code, which is the whole point of a security check.
Signal's CTO, Ehren Kret, put it this way: "Using AI agents to translate live code into valid Lean theorems is a major breakthrough."
Does this mean Signal can't be hacked?
No. The proofs cover specific security properties of Signal's core cryptographic code, as written in specifications that people chose and reviewed. They don't cover the whole app, your phone, a weak passcode or someone reading your screen over your shoulder. The open-sourced proofs on GitHub let other experts check the work.
For now it's research. DeepMind's announcement doesn't offer AlphaProof Code as a product you can sign up for.
X reactions
One early reaction got the scope right.
DeepMind says AlphaProof Code verified key security properties of Signal's libsignal code, down to compiled ARM64 instructions.
— Buse Nur Yurdakul (@busenur038) November 10, 2026
The proof covers human-reviewed specifications and assumptions, not the entire Signal app. Artifacts are open for review. @GoogleDeepMind
Our take
Most AI security news lately has been bad news, like the stolen AI keys in the Railway breach. This one points the other way. If AI can turn years of proof work into weeks, "mathematically checked" could become normal for the code that guards banking, health records and private chats, not a luxury for a handful of projects.
We'd keep expectations sized right, though. A proof is only as good as the specification behind it, and humans still chose what to prove. For everyday users, the practical lesson hasn't changed: pick apps with strong encryption, keep them updated, and lock your phone.
— Artificially Nerdy
What to do now
Nothing yet. Keep Signal or Google Messages updated as usual; this research doesn't change how you use them.
FAQ
What is Lean?
Lean is a programming language for writing mathematical proofs. A computer checks every step, so a proof only counts once every step passes that check.
Which apps use the Signal protocol?
DeepMind names the Signal app and Google Messages. The protocol protects what DeepMind calls "billions of private conversations."
Can other companies use AlphaProof Code?
DeepMind hasn't announced it as a product. It open-sourced the verification artifacts for the Signal work and says scaling the method needs more research. It mentions medical device firmware and power grid software as future targets.
Which AI model did the proofs?
Agents powered by Gemini Carbon, one of Google's Gemini models, wrote the proofs.
Sources
- Google DeepMind: Introducing AlphaProof Code — November 10, 2026; method, six million lines of Lean, four weeks, ~1% human review, two reintroduced bugs, Ehren Kret quote.
- Google DeepMind code-verification on GitHub — open-source proof artifacts.
- Wired: A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure — November 10, 2026.
- Buse Nur Yurdakul on X — November 10, 2026, 11:37am ET.
