AlphaProof Code verified Signal's protocol in four weeks: what DeepMind proved and what it did not

Google DeepMind says a new system called AlphaProof Code has mathematically proved key security guarantees in the code behind Signal, one of the most widely used encrypted messaging protocols. The announcement landed on November 10, 2026. It is one of the more concrete examples of a frontier lab pointing AI agents at a hard, checkable problem instead of a benchmark, and it deserves a careful read of what was and was not shown.

What DeepMind announced

AlphaProof Code is, in DeepMind's words, an agentic framework for formal verification. Formal verification means writing down exactly what a piece of software must do, then producing a proof, checked by a machine, that the code does it. DeepMind's post, written by Pushmeet Kohli and Swarat Chaudhuri, says humans decide what to prove and a group of AI agents does the proofs. The agents run on Gemini Carbon, and the proofs are written in Lean, a proof assistant language. Lean is an open-source proof assistant, and a proof in it is accepted or rejected by the checker with no room for opinion.

The target was the Signal protocol. The properties include keeping messages protected before and after a device is temporarily compromised, a guarantee cryptographers care about a great deal. Researchers used a mix of models to turn Signal's security goals into formal specifications, and human experts reviewed every specification. Agents then generated proofs that the compiled code meets them. DeepMind stresses that most earlier protocol verification stopped at the design level, while this work reached the implementation.

The numbers behind the claim

DeepMind reports four figures worth holding onto. The work took about four weeks. The agents generated more than six million lines of Lean. Only about 1% of the codebase was flagged by the agents for human review. And in a test of detection, two real bugs that Signal had already fixed were reintroduced into an isolated version of the code, and in both cases the system produced a machine-checked proof that the buggy version was insecure.

That last test matters because a verifier that can only say yes is not much use. A tool that rejects known-bad code is at least discriminating. WIRED reported the same pattern: run on older Signal versions with long-fixed vulnerabilities, AlphaProof Code correctly identified them and showed the protocol could not be verified.

What it did not show

WIRED's reporting adds the caveats the blog post leaves quieter. The DeepMind analysis did not find any new vulnerabilities in the portions of the Signal protocol it examined. It did not formally verify the entire Signal mobile app. The researchers also got a head start from earlier formal verification work by the Signal Foundation. Google conducted the analysis free of charge as a research project, declined to share what it cost, and declined to say whether it plans a commercial formal verification product.

The two "firsts" DeepMind claims, first AI verification of a widely deployed cryptographic protocol at this depth and first verification of the implementation of such a protocol by any method, are the company's own assertions. Nobody outside Google has assessed them in print yet. Signal's chief technology officer, Ehren Kret, gave a supportive statement to WIRED: "While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion." That is an endorsement from the party that benefits from the result, which is useful but not independent replication.

Why a lab race story belongs here

This title tracks frontier labs as a race, and the Signal result is a capability signal of a specific kind. Writing a proof that a compiler accepts is a task with an unambiguous grader. Either the proof checks or it does not. That makes it one of the few places where an AI claim can be audited by anyone with the released files, and DeepMind says it is releasing the specification and proof for the Signal analysis.

It also speaks to a live argument about AI and cybersecurity. Labs have spent the autumn describing models that find software flaws, and critics have questioned how many of those findings hold up. Anthropic's Project Glasswing is the sharpest example of that dispute. Verification is the mirror image: instead of finding some bugs, it aims to rule out whole classes of them. Kohli told WIRED that banks and other companies "could now say, 'I can prove these properties.'" The word "could" carries weight, because nothing yet shows the method scales or what it costs.

The human part is the point

Chaudhuri was blunt about how the team sees the division of labor. "We don't want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self-written," he told WIRED. "There's a middle ground." The design reflects that: people own the specifications, because a proof only guarantees what the specification says. If the specification is wrong or incomplete, a flawless proof proves the wrong thing. DeepMind has human experts review each one, and the roughly 1% of flagged code goes to people too.

That is the part to watch as this spreads. Earlier this month we covered Claude's formal verification of 123 libraries, where "verified" meant a narrow property, no crash within a memory bound. The Signal work targets richer properties, but the same discipline applies: ask what was specified, who checked it, and what sits outside the box.

What we would watch

Three things will tell us whether this is a milestone or a demo. First, whether the released specifications and proofs are complete enough for outside teams to rerun and extend. Second, whether anyone other than Google reproduces a comparable result on another protocol. Third, cost and access: a method that needs a frontier lab's agents and weeks of expert time is a research instrument, while one that a mid-size security team can afford changes how critical code gets built.

Our position is that the Signal result earns real credit and a measured reading. It shows AI agents can do substantial, checkable proof work under human supervision. It does not show that software is about to become provably safe, that the method is cheap, or that Signal had a hidden weakness. Until the artifacts are open and someone else reproduces the work, the headline number to remember is the one DeepMind itself leaves with a caveat: four weeks, on one protocol, free of charge, at a cost nobody will name.