Five researchers and a crowd of AI agents needed four weeks to prove key security guarantees in Signal’s encryption code. Google DeepMind says this kind of work used to take expert teams years. The proofs check the compiled machine code itself, not just the protocol design on paper.
The tool is called AlphaProof Code. Google DeepMind announced AlphaProof Code on its blog on November 10, 2026. The result matters well beyond Signal, because variants of the Signal Protocol also protect chats in WhatsApp, Messenger and Google Messages. Still, the proofs cover one specific build, and they leave several real-world risks untouched.
What Google DeepMind actually proved
The team verified libsignal, Signal’s core cryptography library. It tested version 0.105.4 with SPQR 1.6.0, built into a small command-line test program called libsignal-cli. That code is about 560 KB, or roughly 140,000 instructions for 64-bit Arm (AArch64) chips.
The proofs cover two parts of the protocol. PQXDH is the handshake that sets up a new secure session. Triple Ratchet is the system that keeps changing the keys as messages flow. Together, they handle starting a chat, sending messages and receiving them.
According to the AlphaProof Code technical paper, the proven properties include:
- Message confidentiality and authenticity.
- Forward secrecy, so stolen keys do not expose older messages.
- Post-compromise security, so protection can recover after a device is briefly compromised.
- Handshake secrecy, even if a future quantum computer later breaks the Diffie-Hellman math used in the handshake.
The attacker in this model controls both the network and the Signal server. It can also steal long-term keys, prekeys and session data.
What changes for you
For a Signal user, nothing changes on the phone today. No app update is involved. The news is about confidence: the code that runs Signal’s core encryption now has machine-checked proof that it does what its design promises.
Signal CTO Ehren Kret called the work “a major breakthrough” in the DeepMind announcement. He said earlier verification efforts focused on smaller scopes. He added that this rigor gives Signal more confidence in its privacy guarantees.
WhatsApp, Messenger and Google Messages users should read the result more carefully. Those apps use variants of the protocol, but the proofs do not cover their code. The same is true of Signal’s own mobile apps. The paper notes that Signal for Android and iOS run the same Rust libsignal code. The theorems may carry over only if those environments preserve the code’s behavior.
In short, strong proof of the encryption core does not equal proof that a whole app is safe.
Covered and not covered
The paper lists its limits openly. Here is a summary based on the paper and the project’s public verification page.
| Area | Status |
|---|---|
| One-to-one chats (PQXDH plus Triple Ratchet) | Covered |
| Compiled AArch64 machine code of the test build | Covered |
| Quantum attacker breaking Diffie-Hellman after the handshake | Covered in the symbolic model |
| Group chats | Not covered, left as future work |
| Multiple devices per account | Not covered |
| Side channels and other secrets in memory | Out of scope |
| Quantum attackers in the computational proof | Not covered, classical attackers only |
| SPQR post-quantum healing | Not covered |
| Key generation step (keygen) | Not verified |
| Signal’s Android and iOS apps | Not directly verified |
The proofs also rest on assumptions. They treat cryptographic building blocks such as hashes and signatures as secure. They also trust 37 hooked routines, mostly cryptographic primitives, whose own code was not verified. The paper adds that its computational bound becomes meaningless for very many long sessions.
The Register noted that the result assumes perfect cryptography. Even so, it called the work “still a meaningful assertion of correctness.”
How humans and AI split the work
Humans decided what to prove. Models then turned Signal’s security goals into formal statements in Lean, a language that checks math proofs by machine. The paper says Gemini 4 Carbon and Claude Opus 5.5 powered this specification step. Human experts reviewed every specification.
Agent teams powered only by Gemini 4 Carbon wrote the proofs. A team typically had 40 to 80 agents and ran for 24 to 72 hours on one machine. In total, they produced about 6.5 million lines of machine-checked Lean proof.
Auditor agents then flagged about 1% of the work for human review. The Lean kernel checks the rest on its own, independent of any AI model.
Lead researcher Swarat Chaudhuri told The Register that the hard part is now deciding what to prove. “The next frontier is not going to be proof but specification,” he said.
Technical details: bug tests and earlier analysis
Two old bugs put back on purpose
To test the system, the team reintroduced two real libsignal bugs that had already been fixed. The first was an archived-session bug. A failed prekey message could be decrypted against an older session, and the new session state was then stored with a copy of the signed prekey’s secret.
The second was a small-subgroup bug. The PQXDH responder did not check that the initiator’s X25519 base key was valid. A replayed handshake with a mangled key could then create a second session with the same shared secret. For both bugs, Lean proofs showed that the broken builds violate the security theorems.
Problems in a prior paper
The work also turned up 15 gaps or bugs in an earlier academic, computational analysis of the Double Ratchet. The paper describes them as missing hypotheses and game conditions that allowed trivial wins. These were flaws in that analysis, not in Signal’s shipping code.
The machine model
The team built a Lean model of user-mode AArch64 Linux. It covers 467 instructions and 31 system calls in 7,578 lines. They tested it against the Unicorn emulator, Arm’s Sail model and qemu-aarch64.
Context and what to watch next
The project is a step toward a challenge the Beneficial AI Foundation issued in April 2026. That challenge asks for formal verification of the Signal protocol and app using Lean. The Register notes that the seL4 microkernel proof took 20 person-years, which shows how much faster this effort ran.
Several questions remain open. Google DeepMind has not disclosed the cost of the project. The Register only reported that it used “quite a few tokens.” The company has not announced a product launch for AlphaProof Code either.
The blog points to future targets such as medical device firmware and power grid software. It also suggests pairing the approach with CodeMender, DeepMind’s AI code-security agent. Google DeepMind admits that scaling up “requires continued research.” Group chats and multi-device support are the obvious next tests for Signal itself.
The team has open-sourced its Lean proofs and tooling, so outside experts can inspect the work. The researchers’ claim that this is a first has not yet been checked independently.
