Google DeepMind says AI agents verified Signal code in four weeks

Google DeepMind published a technical announcement on November 10, 2026 with a claim specific enough to be checked: a group of AI agents had produced machine-checked mathematical proofs that the compiled code behind the Signal protocol satisfies key security properties. The protocol protects messaging in Signal and also underpins Google Messages and WhatsApp, according to WIRED. DeepMind described the result as the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth, and the first time such a protocol's implementation has been verified by any method, with or without AI.

Formal verification has always been the expensive branch of software assurance. Rather than test a program and hope that untested paths behave, engineers state in mathematics what the code must do and then prove that the real code satisfies the statement, with a proof assistant checking every step. The approach has produced landmark results at a cost measured in years of expert effort. The verified microkernel seL4, a common reference point for this work, absorbed roughly 20 person-years, which helps explain why verification has stayed in high-assurance niches.

AlphaProof Code is DeepMind's attempt to change that arithmetic. The company describes it as a multi-LLM agentic framework that splits verification the way a research team would: human experts work with AI to decide what should be proved, and a group of AI agents does the proving. For the Signal project, researchers first worked with a mixture of models to translate Signal's security goals into formal mathematical specifications, and human experts reviewed every one of them.

The target was not a toy model. Researchers wrapped the unmodified libsignal v0.105.4 and SPQR v1.6.0 crates in a small command-line harness, then used stock rustc to build a statically linked AArch64 Linux executable. The proof therefore aimed at the machine code that would run on devices rather than at an abstract sketch of the protocol. The verified scope was one-to-one session code covering the PQXDH handshake and Triple Ratchet messaging, establishing forward secrecy, authentication, post-compromise security and handshake secrecy.

Key Facts

DeepMind said its agents generated more than six million lines of machine-checked Lean proofs. Unite.AI reported on November 10, 2026 that the total came to about 6.5 million lines, resting on roughly 26,000 lines of trusted specifications and AArch64 semantics. ADTmag reported on November 10, 2026 that the technical report describes verification at the AArch64 machine-code level for properties of Signal's PQXDH handshake and Triple Ratchet, with guarantees that include authentication and protections for message secrecy after a device is compromised.

The project took four weeks. Unite.AI reported on November 10, 2026 that a five-person research team finished the proof work in that window, pursuing symbolic and computational proofs in parallel. Typical campaigns used 40 to 80 agents on one machine for 24 to 72 hours. Agents powered by Gemini 4 Carbon and Claude Opus 5.5 drafted and reviewed the specifications, Gemini 4 Carbon agent teams generated all of the proof code, and none of the authors wrote proof code, according to that account.

DeepMind says the agents audited the proof and highlighted areas that needed a second human look, and that this flagged share came to just one percent of the codebase. That number is the operational heart of the pitch: the machine does the volume, and people concentrate on the places where a mistake would be most consequential or most likely.

To check whether the specifications could catch real errors, the team reverse-applied fixes for two previously repaired libsignal bugs, known as weak state and small subgroup, in an isolated copy of the code. In both cases the system produced Lean proofs that the symbolic security theorem failed. WIRED reported on November 10, 2026 that running AlphaProof Code on older Signal versions with known, long-fixed vulnerabilities correctly identified them and showed the protocol could not be formally verified. The analysis found no new vulnerabilities in the portions it examined.

Signal CTO Ehren Kret said in Google's announcement that the approach enables significant expansion, and that using AI agents to translate live code into valid Lean theorems is a major breakthrough. WIRED reported on November 10, 2026 that the researchers got a head start from past formal verification work by the Signal Foundation. Pushmeet Kohli, DeepMind's vice president of research and chief scientist at Google Cloud, framed the value in commercial terms, saying banks and other companies that rely on assurances could now say they can prove these properties.

Analysis

The caveats are as important as the claims. WIRED reported on November 10, 2026 that the analysis did not formally verify the entire Signal mobile app, and DeepMind researchers described the result as one milestone in a larger process. Swarat Chaudhuri, a DeepMind research scientist, told WIRED that the team is very excited but that there is a long distance to go before the approach scales to all the software of the world. Group messaging was left for future work, key generation was not verified, and side channels and multi-device state fall outside the scenario.

There is also a specification problem that no proof assistant solves. ADTmag reported on November 10, 2026 that Lean can reject an invalid proof but cannot decide whether a human-approved statement captures the security requirement that matters, so a mistaken specification can leave a perfectly proved system unprotected. What this really means is that the scarce skill in automated verification is not proof construction but the judgment about what deserves to be proved, and that judgment still sits with people who must be right about the threat model.

The cost question remains open. DeepMind ran the Signal analysis free of charge as a research project, Google declined to share the cost, and it declined to comment on whether it plans a commercial formal verification product or service, according to WIRED. The bigger picture here is that a four-week proof only becomes an industry practice if the price per release falls far enough for vendors to repeat it, and nobody has published that number yet.

The comparison that matters is not four weeks against 20 person-years in the abstract. It is four weeks against the release cadence of real software. If verification can follow a library through version bumps, it changes how maintenance works; if each campaign is a bespoke research project, it remains a demonstration of what is possible rather than a change in how code is shipped.

Why It Matters

Signal is not a niche product. The protocol's guarantees are relied on across several messaging applications, and independent validation of the implementation is different in kind from a vendor promising that its code is sound. A machine-checked artifact can be replayed by a third party, which is a stronger form of assurance than a model reporting that software looks correct.

The result also gives DeepMind a platform argument. The company frames the work as groundwork for securing medical device firmware and power grid software alongside automated defense agents such as CodeMender. Those are environments where a proven property is worth more than a test suite, and where the cost of expert verification has historically kept formal assurance out of reach for all but the best funded projects.

For the cryptography community, the value is partly negative: the analysis found no new vulnerabilities in the code it examined, and the failures it surfaced were in older versions whose flaws were already known and fixed. That is a useful result. It suggests the tool is not inventing problems, while the bug reinsertion tests suggest it is not blindly blessing whatever code it receives.

Next Up

The stated research goal is verifying new libsignal releases before they ship, which Unite.AI reported on November 10, 2026 is a goal rather than an announced deployment. Group messaging, key generation and side channels are the obvious next targets. Whether the post-quantum healing that SPQR is designed to add can be proved is also unresolved by the current arguments, and the computational model becomes vacuous at large message and session scales.

DeepMind says it is open-sourcing its formal verification artifacts, which gives outside researchers something to replay and attack. The unanswered question is whether Google turns the capability into a product, and at what price. Until then, the Signal proof stands as a carefully bounded milestone: real code, real machine code, a real four-week timeline, and a long list of properties it does not yet cover.