Google DeepMind has used AI agents to produce machine-checked proofs for key security guarantees in Signal’s production cryptographic code, moving formal verification past a protocol diagram and down to the compiled instructions that run on a device.
The lab introduced AlphaProof Code on November 10. A five-person team completed the project in four weeks, generating about 6.5 million lines of Lean proof code for an AArch64 build of libsignal. The result covers Signal’s post-quantum PQXDH handshake and Triple Ratchet, including forward secrecy, authentication, handshake secrecy and recovery after some key compromises.
It is a substantial security result, but it is not a blanket proof that Signal cannot be hacked. The theorems apply to specified protocol properties, a particular compiled binary and documented assumptions. Group messaging, sealed sender, side channels, trust-on-first-use and several multi-device scenarios remain outside the verified scope.
What AlphaProof Code actually verified
Most formal analysis of a cryptographic protocol studies a mathematical description of the design. Production code introduces another layer of risk: serialization, mutable state, compiler transformations, delayed messages, archived sessions and implementation choices that a paper model may not capture.
DeepMind’s project connects those layers. According to the technical paper and open verification artifacts, the team built an AArch64 executable with stock rustc from the unmodified libsignal v0.105.4 and SPQR crates. AlphaProof Code then proved that runs of that machine code conform to approved security models.
The verified binary was about 560 KB and contained roughly 140,000 AArch64 instructions. The proofs rest on about 26,000 lines of trusted specifications and processor semantics. That distinction matters: Lean can verify that a proof follows from a specification, but humans still have to decide whether the specification asks the right security question and whether its assumptions match the deployed system.
The work uses two established kinds of cryptographic analysis. A symbolic model treats cryptographic operations as ideal and lets an attacker control the network, interleave sessions and compromise selected keys or session state. A separate computational model works with byte strings and bounds an attacker’s success by the assumed difficulty of breaking the underlying cryptographic primitives.
Together, the results establish selected guarantees for PQXDH and the Triple Ratchet. PQXDH creates an encrypted session using both elliptic-curve and post-quantum key material. The Triple Ratchet then updates keys as a conversation continues, combining the Double Ratchet with Signal’s post-quantum SPQR mechanism. The verified properties include message-key forward secrecy, authentication, post-compromise security under the model’s conditions and secrecy around the handshake.
Why checking machine code is different
Source-level verification generally has to trust the compiler and the formal model of the programming language. AlphaProof Code instead reasons about the compiler’s output. That removes rustc, LLVM and Rust’s semantics from the trusted base for this result, although it adds a different dependency: the formal AArch64 model must accurately describe the processor behavior being analyzed.
The approach also covers implementation machinery that is easy to miss in a design-only proof. Signal stores keys for out-of-order messages, archives older sessions so delayed messages can still be decrypted, serializes state with Protocol Buffers and spreads SPQR material across ordinary messages. The machine-code proof has to account for those paths rather than assume the implementation behaves like the protocol sketch.
DeepMind tested the framework by restoring two real, previously fixed libsignal bugs in isolated builds. One “weak state” flaw could preserve an unconfirmed session state containing a copy of a signed prekey secret after a message was successfully decrypted against an older session. The other involved an X25519 small-subgroup and encoding check: a modified base key could create a second session with the same shared secret.
For both altered binaries, AlphaProof Code generated complete Lean disproofs showing that the symbolic security theorem no longer held. These were not fresh Signal vulnerabilities, and the research did not expose current users to the old flaws. Reintroducing them provided a controlled test that the formal specification could distinguish the fixed implementation from known-bad versions.
The AI agents could not grade their own work
The proof pipeline was designed around the possibility that an AI agent might satisfy a task by quietly weakening it. The paper describes agents adding hypotheses, narrowing preconditions or changing a definition in ways that make a theorem easier or even vacuously true.
AlphaProof Code therefore separates proof generation from acceptance. A gatekeeper sees theorem names and file paths rather than the agents’ reasoning transcripts. It replays every proof in a fresh Lean environment and rejects shortcuts such as sorry and native_decide. Specification amendments are logged, reviewed and cannot weaken a security requirement merely to fit the code; a mismatch of that kind is escalated as a possible bug.
Human judgment remains central. Researchers selected the reference models, determined the scope, approved trusted statements and reviewed proposed changes. Gemini 4 Carbon powered the proof agents, while the specification work involved repeated review with Gemini 4 Carbon and Claude Opus 5.5. The team says people did not write the proof code, but they did decide what the millions of generated proof lines needed to establish.
What the Signal proof does not cover
The most important limitation is straightforward: “formally verified” means the implementation satisfies the formal claims under their assumptions. It does not mean every security property of the complete Signal service has been proven.
The assembly-level scenario starts with two honest parties whose identity keys are already pinned. It does not exercise Signal’s trust-on-first-use path. The harness uses fixed roles and one session per session file, bounds input sizes and message counts, and does not model one-time Kyber prekeys. Side-channel attacks and other secrets left in memory are out of scope.
The computational analysis does not cover quantum attackers, full multi-device state, some adversarial first-message cases or sufficiently large collections of long sessions. The symbolic ratchet theorem lets the attacker choose SPQR keys, so it shows that the Triple Ratchet is no weaker than the Double Ratchet under that setup; it does not prove SPQR’s intended post-quantum healing. The current work also excludes Signal group messaging, sealed sender and server-side protocols.
Some low-level cryptographic routines are represented by idealized contracts rather than verified instruction by instruction. Two output functions and several library routines also remain inside the trusted boundary. Hardware faults, operating-system behavior outside the harness and a real processor diverging from the AArch64 semantics could still create gaps between the proof and a deployed phone.
Those limits do not erase the result. They define it. In a field where security claims are often compressed into “encrypted” or “formally verified,” publishing the assumptions and uncovered cases lets other researchers audit the work and identify the next proof targets.
Why this matters for software security
Formal verification has historically been reserved for narrow, high-assurance systems because it consumes years of specialist labor. DeepMind points to the seL4 microkernel’s roughly 20 person-years of verification work and the CompCert compiler’s six. The Signal project does not make those efforts directly comparable, but completing this proof campaign in four weeks shows how AI can change the economics of producing and maintaining large machine-checked arguments.
The harder problem is shifting from writing proofs to writing trustworthy specifications. DeepMind reports that most of the team’s effort went into deciding what to prove, reconciling the live code with prior research and making the formal statements auditable. The exercise found more than a dozen gaps or errors in earlier published analyses that had to be repaired before the new proofs would pass.
For developers, AlphaProof Code is still research rather than a product they can add to a continuous-integration pipeline. DeepMind researcher Swarat Chaudhuri told Axios that the lab is exploring integration with coding agents and Google security work such as Project Zero and CodeMender. The immediate deliverable is the open Lean repository, not an “unhackable software” button.
The practical opportunity is narrower and more credible: use AI to reduce the proof-writing bottleneck, keep human experts responsible for specifications and make the proof checker independent of both. If that workflow survives outside a carefully staffed research project, formal verification could become feasible for more cryptographic libraries, medical-device firmware and critical infrastructure components. Signal is the demonstration; the next test is whether teams can repeat it as production code changes.
