AlphaProof Code Mathematically Verifies Signal's Encryption Code
DeepMind's AI agents wrote 6.5 million lines of checked proof in 4 weeks to show Signal's code keeps its promises. Here is what it covers and what it doesn't.
Hakkı ALKANPublished 4 min read
Google DeepMind on Tuesday, Nov. 10, 2026, unveiled AlphaProof Code, a team of AI agents that mathematically proved key security properties of libsignal, the code behind the Signal protocol. The agents produced about 6.5 million lines of machine-checked proof in four weeks, a job DeepMind says used to take expert teams years.
The Signal protocol protects billions of private chats in apps like Signal and Google Messages. DeepMind claims this is the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time the actual implementation of such a protocol has been verified by any method, as it explains in its AlphaProof Code announcement.
What is formal verification, and why is it hard?
Formal verification means proving with math that a program does exactly what its specification says, for every possible input, instead of just testing it on some cases. It is the gold standard for security, but it is slow and expensive, so it is usually reserved for small, critical pieces of code.
The proofs here are written in Lean, a programming language that doubles as a strict proof checker. Lean checks every single step, so a proof written by an AI agent is only accepted if the checker signs off on it. That matters, because it means nobody has to take the AI's word for anything.
How does AlphaProof Code work?
The work is split the way a research team would split it. Human experts worked with several AI models to turn Signal's security goals into formal specifications, and the experts reviewed every one. Then prover agents running on Gemini Carbon wrote the proofs, and a final audit pass flagged about 1% of the work for a human second look.
The key difference is depth. Most protocol proofs stop at the design on paper. DeepMind compiled libsignal with the standard Rust compiler into 64-bit Arm (AArch64) machine code and proved the properties against that compiled code. According to the AlphaProof Code technical paper, the 6.5 million lines of proof rest on about 26,000 lines of trusted specifications and machine-code rules.
What exactly did it prove about Signal?
The proofs cover Signal's post-quantum PQXDH handshake, which is how two phones agree on keys, and the Triple Ratchet, which keeps changing those keys as you chat. The verified properties are:
- Forward secrecy: if a key leaks later, your older messages stay safe.
- Post-compromise security: if a device is briefly compromised, the conversation heals and future messages become safe again.
- Authentication and handshake secrecy: you are talking to the right person, and the starting keys stay secret.
As a sanity check, researchers put two real, long-fixed Signal bugs back into an isolated copy of the code. In both cases, the system produced a machine-checked proof that the buggy version was insecure. No new vulnerabilities turned up in the parts examined, Wired reported.
What did Signal say?
Signal CTO Ehren Kret called the approach "a major breakthrough," noting that using AI agents to turn live code into valid Lean theorems goes well beyond earlier, smaller verification efforts. "As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees," he said.
What does it not cover?
This is not a proof that the whole Signal app is bug free. The work covers the core cryptographic protocol code, not the full mobile app, and the low-level crypto building blocks were treated as assumed-secure contracts rather than proven from scratch. The proofs also target one compiled platform, AArch64 Linux.
DeepMind is open-sourcing the specifications and proofs, and it pitches the method for medical device firmware and power grid software next. It fits a wider trend of AI labs pushing their models as defenders, a day after Anthropic said 1,000 agents formalized Fermat's Last Theorem in Lean, as we covered in our Claude Fable 5.2 report.
Our take: this is one of the most convincing uses of AI agents in security so far, because every step is checked by a machine rather than trusted. It is also a counterweight to a week of worrying security news, including DeepMind's RSA-1024 research on faster attacks against older encryption.
Real breaches keep coming too, as the recent Fireworks AI hack showed, so tools that prove code is safe before it ships are exactly what the industry needs more of.
What should Signal users do?
- Nothing new to install: this is extra assurance, not an app update.
- Keep Signal and your phone updated, since bugs outside the verified core still matter.
- Treat it as a strong signal of trust in Signal's encryption design and code, not a guarantee against every attack.
| AlphaProof Code at a glance | Detail |
|---|---|
| Target | libsignal, Signal's reference implementation |
| Proven parts | PQXDH handshake and Triple Ratchet |
| Proof language | Lean |
| AI model | Gemini Carbon agents |
| Proof size | About 6.5 million lines |
| Trusted base | About 26,000 lines |
| Time taken | Four weeks |