DeepMind's AlphaProof Code verifies Signal encryption in machine code

Felix Laurent 10 Nov 2026 6 min read

AI agents

Google DeepMind says its AI agents have formally verified key security properties of Signal's encryption code, down to the compiled machine code. The lab announced the system, called AlphaProof Code, on November 10, 2026. Agents powered by Gemini 4 Carbon wrote about 6.5 million lines of Lean proofs in four weeks. None of the human authors wrote proof code.

DeepMind vice president Pushmeet Kohli called it the first time production code of a widely deployed protocol was verified at this depth by any method. Formal verification has usually been too slow and costly for code of this size. DeepMind argues that AI agents change that math.

What DeepMind verified in Signal

The target was libsignal, the Rust library behind Signal's one-to-one encryption, at version 0.105.4. It covers two parts:

PQXDH: the handshake that sets up a session, with a post-quantum key exchange
Triple Ratchet: the Double Ratchet plus SPQR, which keeps changing keys as messages flow

DeepMind wrapped the unmodified library in a small command-line program and compiled it for 64-bit Arm Linux. The proofs cover that binary, about 140,000 machine instructions. Because they target compiled code, neither the Rust source nor the compiler has to be trusted.

The agents proved ten theorems in a symbolic model, where the attacker controls the network. They include forward secrecy, which protects past messages if keys leak, and post-compromise security, which restores privacy after a breach. A separate proof gives a concrete bound on an attacker's odds under standard cryptographic assumptions. The paper also shows every verified run ends without memory faults.

Signal's CTO Ehren Kret welcomed the result in DeepMind's blog. "Using AI agents to translate live code into valid Lean theorems is a major breakthrough," he said. Getting there took a specific division of labor between people and agents.

How AlphaProof Code works

The system runs in three stages, and only some of its parts are trusted.

Google DeepMind's AlphaProof Code: agents and humans write a Lean spec, code runs on a Lean model of the processor, and a gatekeeper checks proofs — Diagram: Google DeepMind, November 10, 2026

First, humans and agents write a specification in Lean, the language that states what "secure" means. Spec drafts came from agents running Gemini 4 Carbon and Anthropic's Claude Opus 5.5. A reviewer from a different model family checked each draft, and humans approved every one.

Second, the compiled binary runs on a model of the Arm processor written in Lean. That model covers 467 instructions and 31 system calls in about 7,500 lines. DeepMind tested it against two independent Arm emulators, replaying 15.6 million instructions with matching results.

Third, a prover team of 40 to 80 agents worked on one machine for one to three days per campaign. Its roles included workers, team leads, an architect and a critic. A gatekeeper then compared each proof against a held-out copy of the spec and rejected any shortcuts.

That gatekeeper matters because agents cheat. The paper notes cases where agents weaken their goals, including one swarm in earlier research that redefined a property as False. In its words, "once proofs become cheap, the hard question is what to prove."

The proof base breaks down by part:

DeepMind's Signal proof: 6.5 million lines of Lean, 5.3 million on the binary, versus 13 million for Anthropic's Fermat proof — Figures from DeepMind's AlphaProof Code paper and the cited projects, 2026

People still need to read about 26,000 lines of trusted code and specs, according to DeepMind. The blog says agents flagged about 1% of the codebase for a second look by a human. That figure does not appear in the paper, which says humans reviewed every specification. The next question is whether the proofs would catch a real flaw.

How DeepMind tested the proofs on real bugs

To check that the proofs mean something, the team reintroduced two bugs that Signal had already fixed. Both came from a 2026 paper by Cheval, Jacomme and Richards, who found them with the ProVerif tool.

One was a "weak state" bug, where an old session could store a copy of a secret key. The other let an attacker replay a session by sending a malformed curve point. For both, the agents produced Lean proofs that the security theorem fails on the buggy binary.

According to secondhand reports of Wired's coverage, the effort found no new vulnerabilities in current Signal code. It did find 15 gaps or errors in an earlier academic analysis of the Double Ratchet. It also found mistakes in printed queries from another paper.

Those results come with a long list of limits, which DeepMind spells out itself.

What the verification does not cover

The proofs concern DeepMind's own build of the library. The paper says they carry over to Signal's Android and iOS apps only if those apps preserve the same behavior. Key generation was not verified, and the theorems take keys as given.

Other gaps are larger:

Crypto primitives: 39 routines, including AES, SHA-2, X25519 and Kyber, are replaced by trusted contracts
Side channels: timing attacks are out of scope
Scenario: two honest parties, one session per file, no group chats, no multiple devices
Quantum attackers: SPQR's post-quantum healing is not proved, and the computational bound is classical only

On Hacker News, where the post drew 259 points, readers focused on these gaps. "This didn't verify the Signal app, only the signal encryption protocol," one user wrote. Another worried that AI could cheat, since it also writes the Lean. DeepMind researcher Swarat Chaudhuri told Wired there is "a long distance to go" before the method scales to all software, according to Startup Fortune.

Even with those limits, the result lands in a busy year for AI-written proofs.

AI agents and formal verification in 2026

Signal was already a target. In April 2026 the Beneficial AI Foundation, Signal and the Lean community launched the Signal Shot challenge to verify the protocol in Lean. DeepMind's paper says its results would have taken "years of expert labor with earlier tools."

Earlier this year, Anthropic's Claude agents formalized Fermat's Last Theorem in about 13 million lines of Lean in 11 days. Anthropic and Theorem later proved hundreds of open-source entry points crash-free. Last week, Axiom formalized the Stacks Project in about 16 million lines of Lean.

For Google, the work also shows off Gemini 4 Carbon, its strongest model. Google released it on October 28 to a limited group of cyber defenders. Days earlier, DeepMind agents found new attacks on older 1,024-bit RSA keys. Its CodeMender agent has been fixing open-source code since 2025.

What the Signal proof means for software security

For security teams, the result shows that machine-checked proofs of real, compiled code are now a matter of weeks. A team of five people with agents did work that once took experts years. The proofs, specs and processor model are open source on GitHub under Apache 2.0, so other researchers can check them.

The hard part has moved from proving to specifying. A proof is only as good as the spec it checks. Signal is also close to a best case, with a small, well-studied protocol and years of prior analysis. DeepMind has not said what the run cost or whether it will sell the tool. The method now needs to work on messier code with no clear spec, such as the firmware and grid software Kohli named as next targets.

Update, November 10: Google CEO Sundar Pichai shared the result on X a few hours after DeepMind's announcement. He framed it as a step toward "scalable formal verification" that could "shift the advantage to defenders" in software security. He also confirmed that Google is open-sourcing the results for the security community.