AlphaProof Code Verifies Signal Down to Machine Code

Google DeepMind has introduced AlphaProof Code, an agentic framework for formal verification, and its first target was the code behind Signal’s encrypted messaging. In a research post by Pushmeet Kohli and Swarat Chaudhuri, DeepMind says the system produced a machine-checked proof that Signal’s compiled code delivers key security properties, such as keeping messages protected both before and after a device is temporarily compromised. Cryptographers call those guarantees forward secrecy and post-compromise security. DeepMind describes the result as the first time AI has formally verified a widely deployed cryptographic protocol at this depth, and the first time an implementation of a protocol like this has been verified by any method, with or without AI. Those are the lab’s own claims.

Formal verification means proving, mathematically, that a program does what its specification says, rather than testing it and hoping the tests were good enough. The proofs here are written in Lean, a language whose checker accepts a proof only if every step holds. The catch has always been labour: according to DeepMind, expert teams have historically needed years to verify software of this kind. AlphaProof Code finished in four weeks.

The framework splits the work the way a research team would. First, researchers used a mix of models to turn Signal’s security goals into formal specifications, and human experts reviewed every one of them. Second, a team of prover agents running on Gemini Carbon, Google’s newest frontier model, wrote the proofs: more than six million lines of Lean. Third, the agents audited their own output and flagged the parts that deserved a second look from a person, which DeepMind puts at about 1 percent of the codebase. Lean checks the rest automatically. The key design choice is that nothing an agent writes is trusted until the checker accepts it.

What makes the depth unusual is the target. According to the README of the released artifacts, the proofs cover the compiled AArch64 machine code of libsignal, the library Signal’s apps are built on, rather than a simplified model of the protocol. There are two of them: one in the symbolic model of cryptography and one in the computational model, which the authors say give independent arguments for security. DeepMind’s point is that the gap between a protocol’s design and the code that ships is where real vulnerabilities tend to hide. To test that the method catches them, the team put two real, previously fixed bugs back into an isolated copy of Signal’s code; in both cases the system produced a machine-checked proof that the buggy version was insecure.

Signal took part. DeepMind thanks Signal’s Rolfe Schmidt, Michael Rosenberg and Ehren Kret for feedback on the methodology, and quotes Kret, Signal’s chief technology officer, calling the agents’ translation of live code into valid Lean theorems “a major breakthrough.” He adds that, as AI-driven threats grow, this kind of verification gives Signal even greater confidence in its privacy guarantees. Signal’s own blog had not posted about the work when this article was written.

The scope has limits that the announcement states or implies. The proofs cover key security properties, not every behaviour of the library; the README says they run through a command-line harness with hooked cryptographic primitives; and DeepMind says scaling the techniques needs more research. Rebuilding the proofs is heavy work, too: the README warns of several hours and roughly 15 to 34 GiB of peak memory. The artifacts are open-sourced under the Apache 2.0 licence, with the copied libsignal code keeping its AGPL-3.0 licence.

DeepMind frames the result as groundwork for checking other software that cannot be allowed to fail, from medical-device firmware to power-grid control code, and pairs it with CodeMender, its agent that finds and patches vulnerabilities. Finding bugs with AI has become a crowded race; Anthropic’s Project Glasswing counts its zero-days in the thousands. AlphaProof Code makes the opposite kind of claim. It does not say what is broken in the code. It proves what cannot go wrong, and gives the proof to anyone who wants to check it.