DeepMind's AlphaProof Code Verifies Signal's libsignal at Machine‑Code Level

Google DeepMind said Tuesday that its new AlphaProof Code system generated machine-checked proofs for key security properties of Signal’s libsignal implementation at the compiled machine-code level, a notable claim because it targeted unmodified production code rather than a version rewritten for verification.

The announcement came in a DeepMind blog post, “Introducing AlphaProof Code: a breakthrough in verifying complex software at depth,” and a technical paper, “AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level.” The work focused on libsignal, the reference implementation of the Signal protocol, not the full Signal app. DeepMind said the proofs covered the PQXDH handshake and the Triple Ratchet, and that they apply to the compiled AArch64 binary produced from the unmodified code with the standard Rust compiler, rustc.

Formal verification is a method of proving software properties mathematically and having a theorem prover check the proof, rather than relying only on testing. That helps explain why DeepMind’s claim stands out. Major projects such as seL4, CompCert and Project Everest have shown formal methods can secure critical software, but those efforts were historically labor-intensive and often involved systems designed or rewritten with verification in mind. DeepMind’s claim here is different: it says the system worked on a widely deployed cryptographic implementation as it is actually compiled and shipped.

In the paper’s abstract, the authors wrote: “We introduce AlphaProof Code, a multi-agent AI framework for formal software specification and verification that we used to prove key security properties of libsignal, the Signal protocol’s reference implementation, at the machine-code level.”

DeepMind said the resulting proof development totaled about 6.5 million lines of Lean, the programming language and theorem prover used to express and check the proofs. The company said the verification run took four weeks. AlphaProof Code is described as a human-guided, multi-agent framework: humans and software agents help produce formal Lean specifications, prover agents generate proofs, and a gatekeeper together with Lean’s kernel checks them. DeepMind said the agents were powered by Gemini Carbon.

The theorems in the paper establish properties including forward secrecy, authentication, post-compromise security and handshake secrecy. But the result is narrower than a blanket claim that “Signal is secure.” The proofs are machine-checked by Lean, yet they still depend on trusted components, including about 26,000 lines of specifications and AArch64 processor semantics, as well as the underlying cryptographic assumptions built into the model.

DeepMind also said it open-sourced the proofs, specifications, AArch64 semantics, scripts and build instructions in its public project materials and GitHub repository. As a validation test, the company said it reintroduced two previously fixed real libsignal bugs into an isolated version of the code. AlphaProof Code then produced proofs showing that the buggy binaries violated the intended security theorems. DeepMind said the work did not uncover new vulnerabilities in the code it examined.

The paper also makes a broader novelty claim, with attribution: the authors say this is the first machine-checked proof linking protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation.

DeepMind’s blog included a statement attributed to Signal Chief Technology Officer Ehren Kret: “While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion. Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees.”