AI Proved Parts of Signal’s Code. Here Is What That Actually Guarantees

A proof about encrypted messages is only useful if you know exactly what it proves. On November 10, Google DeepMind described using its AlphaProof Code framework to verify selected properties of libsignal, Signal’s reference implementation. The work brings AI agents into a formal-methods workflow, but the assurance still rests on human-reviewed specifications, a defined machine-code model and a deliberately bounded slice of software. ^{[1] [2]}

What the announcement says was checked

The technical paper describes AlphaProof Code as a framework combining a human-guided agent for writing Lean specifications, a formal semantics for AArch64 machine code and autonomous agents that search for proofs. Its case study concerns libsignal, the Rust implementation used by Signal’s client and server projects. The team reports roughly 6.5 million lines of generated Lean proof code, built on about 26,000 lines of trusted specifications and machine-code semantics. Those counts describe the scale of the artifacts, not a count of bugs found or a guarantee about every possible attack. ^{[2] [3]}

The central distinction is between producing a plausible explanation and constructing a proof accepted by a proof checker. In Lean, a theorem is accepted only when its proof term type-checks against the stated definitions and assumptions. The agents can propose and refine proof work; they do not get to declare their own answer correct. That makes the final artifact inspectable in a stronger sense than a natural-language model response.

The paper says the work covers selected properties of the PQXDH handshake and Triple Ratchet, including forward secrecy, authentication and post-compromise security under stated models. The qualifications are substantial: its computational proof covers classical attackers, while the symbolic proof establishes handshake secrecy against a future quantum attacker. The authors explicitly say their ratchet theorems do not prove the post-quantum healing property that the protocol is designed to provide. Their model also fixes some conditions, including one session per handshake and message lengths. These are precise results, but they leave a meaningful set of follow-up theorems and system boundaries open. ^[2]

But a checker only verifies the claim it is given. People must decide which security property matters, what the implementation is supposed to do, which code is in scope and how the machine-level model corresponds to the compiled executable. A proof can be internally sound while the specification omits an important threat or the modeled program differs from the deployed binary.

Why machine-code level matters—and why it is not everything

Formal verification has long been used in cryptography and safety-critical computing. It can connect a precise statement about code to a mathematical argument, reducing reliance on testing alone. Testing samples executions; a proof can establish a property for every execution covered by the model. That is a meaningful difference for code where a rare edge case can undermine confidentiality or authentication.

The DeepMind post says the team reintroduced two previously fixed bugs into an isolated version of the code, and the framework produced checked proofs that the buggy versions failed the intended security property. This is a useful demonstration that the setup can distinguish those cases. It is not an independent benchmark across a representative set of new vulnerabilities, nor does it establish that the process finds every defect. ^[1]

The boundary also matters beyond the cryptographic library. A messaging service depends on client applications, operating-system APIs, update mechanisms, account recovery, key storage, network behavior, server components and the person holding the device. A proof about a cryptographic routine cannot by itself secure a compromised phone or prevent a user from being tricked into sharing a verification code. Signal’s own protocol evolution illustrates that security is maintained over time: new designs and implementations need review as requirements change. ^[4]

AI helps with the labor, not the definition of trust

The practical promise is that agents may make proof engineering less prohibitively slow. DeepMind says the Signal case took four weeks and generated millions of proof lines; the team compares this with work that can take expert groups much longer. That is a company-reported project result, not a general estimate for verifying any codebase. The effort still required cryptography, systems and formal-methods expertise to formulate and review the target properties.

This distinction is important for organizations deciding whether to invest. Formal verification is most compelling when a component is small enough to specify, important enough to justify the work, and stable enough that the proof can be maintained as code changes. An AI agent may help search for a proof, but the team still pays for careful modeling, review, toolchain control and update discipline. A stale proof attached to a changed binary is not assurance.

For security leaders, the useful questions are concrete: Which exact artifact is covered? What theorem was proved? Which assumptions are trusted? Does the build process link the verified source to the shipped binary? Who reviews specification changes? How are updates reverified? These questions make a claim auditable and keep the proof attached to an actual release rather than a headline.

What readers can take from it

Users do not need to change messaging settings in response to this announcement. The research does not identify a newly discovered Signal vulnerability. For developers, it is a reason to learn what proof assistants and machine-checked specifications can offer for high-consequence components. Start with a narrow invariant—such as a key-handling property—and document the threat model, assumptions and exact version under review.

For open-source maintainers, publication of the technical paper and artifacts makes external examination possible. Inspection is not itself independent replication, and the project’s claims should be read alongside its code and specification. The advance is real precisely because it is bounded: AI helped with a hard proof task, while trusted logic and human review remain part of the chain. ^{[2] [3]}

For more on how security claims depend on system boundaries, see our guides to agent permissions and tool access and reproducible builds.