Google DeepMind's AlphaProof Code Mathematically Verifies Signal Protocol Machine Code in 4 Weeks

How far must you verify a cryptographic protocol before you can call it secure? Security researchers have traditionally modeled a protocol's design specification mathematically and proved its security. In real software, however, even a correct design can acquire vulnerabilities when it is implemented as code. A large gap remains between proving that a design is secure and guaranteeing that a running program is secure.

On November 10, 2026, a Google DeepMind research team announced AlphaProof Code, a new formal verification system meant to close that gap. By coordinating multiple AI agents, the team says it mechanically verified that security properties hold under specific conditions for a cryptographic communication library used in messaging apps such as Signal, working on the compiled machine code. Verifying a practical-scale cryptographic implementation down to machine code has traditionally required years of work by teams of experts. DeepMind says it completed this verification in just four weeks.

The result does not mean, however, that the security of the entire Signal app has been mathematically guaranteed. What was verified is a single Linux binary built by combining a specific library with a verification harness, and the proofs rest on cryptographic assumptions and strict preconditions about the execution environment. What did the AI prove, and which parts still depend on human judgment and verification? Based on the published technical documentation, we sort out the achievements and the limits.

Ten security properties proved over roughly 140,000 machine instructions

DeepMind chose as its main target the foundational library of the widely used Signal protocol. Specifically, it used version 0.105.4 of libsignal-protocol, written in Rust, and version 1.6.0 of SPQR, an extension related to post-quantum cryptography. The team made no changes to these existing crates and built them into libsignal-cli, a test harness it developed for verification. It then used the official Rust compiler rustc 1.98.1 to produce a statically linked executable for the AArch64 architecture on Linux.

The finished executable is about 560 KB, equivalent to roughly 140,000 instructions. The scope of verification is limited to session establishment via PQXDH in one-to-one communication and the behavior of the Triple Ratchet protocol, which handles sending and receiving messages. Importantly, what AlphaProof Code verified directly was not the Rust source code but the compiled machine code. The team mathematically described how the binary's instructions execute and proved theorems about that behavior.

This approach has advantages over conventional formal verification that targets source code. Even if correctness is proved at the source level, compiler bugs or optimizations can cause the generated machine code to behave differently from what was intended. Verifying the compiled binary itself removes the need to assume that the compiler produces correct code. In this study, the dependency on the compiler was removed from the trusted base.

Under a symbolic model, the team proved a total of 10 security properties. These include Forward Secrecy, which protects past communications even if long-term keys are later leaked, and Post-Compromise Security, which restores a secure communication state after a temporary device compromise. Handshake authentication, resistance to key compromise impersonation (KCI) attacks, and confidentiality of the handshake itself were also verified. Each of these properties holds only under a defined attacker model and set of environmental conditions.

DeepMind positions this as the first mechanical formal verification of a widely used cryptographic protocol implementation at this level, with or without AI. This is, however, the claim of the announcing party, not a determination made by a third party after comprehensively comparing prior research. In assessing the result, it is necessary to check not only the scale of the proofs but also which behaviors are guaranteed and what is excluded from verification.

The AI generated 6.5 million lines of proof; humans audit a 26,000-line trusted base

A distinguishing feature of AlphaProof Code is how it divides work among human experts, AI agents, and a mathematical proof checker. The verification process falls broadly into three stages, "defining the specification," "constructing the proof," and "checking the proof," each assigned different roles. While the AI generates the proofs, humans remain involved in drawing up the specification of what should be proved and in judging whether that specification is valid.

In the first stage, human experts worked with a specification-writing agent to express the security properties required of the Signal protocol as definitions and theorems in the interactive theorem prover Lean. The research team built about 18,000 lines of specification-dependent definitions and about 8,000 lines of AArch64 instruction-set semantics. Together, these roughly 26,000 lines form the main Trusted Computing Base (TCB) for this verification. A review agent and human cryptography experts checked whether the specification corresponds to the actual security requirements.

Once the specification was fixed, an autonomous proof agent built on the reasoning model Gemini 4 Carbon searched for the logical steps needed to establish the theorems. The result was about 6.5 million lines of Lean proof code, and including related material the full codebase approached 7 million lines. Normally it would not be realistic for humans to check such a vast proof line by line. AlphaProof Code therefore pairs the proof generation with a mechanism that checks the generated proofs mechanically.

Proofs written by the AI are first sent to a checking mechanism called the "gatekeeper." It confirms, among other things, that a proof matches the human-approved definitions and dependencies and that it uses only Lean's standard axioms. Lean's proof-checking kernel then verifies that the conclusion follows logically from the given premises. A proof that fails kernel verification is not accepted, so there is no need to trust the AI-generated arguments unconditionally.

However, Lean's ability to confirm the logical correctness of a proof is a separate matter from whether the specification being proved adequately represents real-world security requirements. If an important attack path were missing from the specification's definitions, then even a completely correct proof against that specification would not necessarily guarantee the security of the actual software. What the proof checker can confirm is only mathematical consistency based on the given definitions and assumptions, not whether the threats that should be considered in the real world have been defined without excess or omission.

Moreover, it is not enough to trust only the roughly 26,000 lines of specification definitions and instruction-set semantics. The proofs also depend on the correctness of Lean's verification kernel itself, the semantics of Linux processes, the contracts of hook functions representing interaction with external systems, assumptions about cryptographic primitives, and the behavior of the tool that extracts code from the binary. On the other hand, verifying the compiled machine code directly made it possible to remove the Rust compiler itself from the trusted base, which is a significant achievement.

The study suggests that the human role in formal verification may change. If AI agents can build proofs of some 6.5 million lines, the burden on experts of assembling vast proof steps by hand will drop sharply. At the same time, the importance of judging whether the specification and trusted base underlying the proof are correct will rise. In other words, the more proof generation is automated, the more the practical challenge may shift from the ability to produce proofs to quality control of the specification: what to prove and under what assumptions. If it can later be shown that specification drafting and trusted-base review can also be automated without adding unaudited assumptions, this picture could change.

Symbolic and computational proofs guarantee different kinds of security

To understand the result correctly, it is necessary to distinguish the two proof approaches the team used: "Symbolic Proof" and "Computational Proof." Both treat the security of cryptographic protocols mathematically, but they differ in the assumptions they make about attacker capabilities and cryptographic primitives. Even if one proof holds, the same guarantee does not necessarily extend to the threats covered by the other.

Symbolic proofs treat cryptographic keys and ciphertexts as abstract symbols and assume that the cryptographic algorithms themselves work ideally. For example, they use a model in which an attacker cannot obtain information about plaintext from ciphertext unless they hold the decryption key. Within this framework, one can verify whether protocol state transitions, key-exchange procedures, and authentication of communication partners work correctly. In this study, the team linked the execution behavior of the compiled binary to this symbolic model and proved 10 security properties.

Real cryptographic algorithms, however, are not mathematically perfect black boxes. Attackers can compute on the bit strings of ciphertexts and try to guess keys or plaintext or to forge signatures. Evaluating such attacks requires considering the computational-complexity security of the cryptography. The team therefore built, separately from the symbolic proof, a proof based on a computational attacker model.

The computational proof depends on several cryptographic assumptions, including the Gap-Diffie-Hellman (Gap-DH) assumption, the unforgeability of XEdDSA signatures, the collision resistance of the post-quantum scheme Kyber1024, and the security of pseudorandom generators (PRGs) and pseudorandom functions (PRFs). It evaluates the protocol's confidentiality and authenticity on the premise that these assumptions hold. A proof therefore does not mean that each cryptographic algorithm is unconditionally secure; if an underlying assumption is broken, the guarantees derived from it must be reconsidered.

Particularly important is that this computational proof does not cover attackers who use quantum computers. The assumptions used in the computational security evaluation presuppose classical computers, and no guarantee is given against attacks by quantum computers. The symbolic proof also handles an abstract model of post-quantum key exchange, but that alone does not amount to verifying against the full range of threats from quantum algorithms breaking cryptography. SPQR's post-quantum state-recovery mechanism is also excluded from the scope of the proof.

The verification environment also has constraints that differ from a real application. First, the verification harness does not itself run key generation; it assumes that the public and private keys of the communicating parties are correctly supplied at setup. Second, in the binary-level verification the peer's identity key is fixed in advance, and the dynamic confirmation procedure of "Trust On First Use" (TOFU), in which the other party's key is trusted at first contact, is out of scope. This means that security has not been proved for the key-confirmation path that arises when the real Signal app communicates with a new contact.

The computational proof also carries mathematical constraints that depend on the volume of traffic and the number of ratchet updates. According to the technical documentation, under extreme conditions in which large numbers of messages are exchanged within a single session and a new epoch is generated each time, the margin in the inequality used to evaluate security is lost. If ratchet updates occur so frequently that a session exceeds roughly 25,000 messages, the computational guarantee reaches its limit. This, however, shows a limit of the bound used in the proof and does not mean the actual cryptography breaks the moment that message count is exceeded.

The verification target is also the libsignal-cli binary running in a Linux environment built by the researchers, not Signal's official smartphone app or the entire runtime environment of Google Messages, which uses the Signal protocol. Threats that can matter in real usage environments, such as inconsistent synchronization state among multiple devices, OS memory corruption, and hardware side-channel attacks, are outside the scope of verification. The result should therefore be assessed as a rigorous guarantee for a specific implementation, not as a comprehensive proof of the security of every product that uses Signal.

Formal verification in four weeks, but computational cost is unknown

Another result DeepMind stresses is how short the verification took. According to the company, AlphaProof Code completed in four weeks work of a scale that previously required years from expert teams. This figure cannot, however, be treated as a general productivity metric implying that any software can be formally verified in a month. According to the paper, five researchers worked on the experiment full time, running AI agents around the clock on their own workstations while carrying out specification drafting and proof search in parallel.

What the AI agents mainly handled autonomously was the proof search needed to establish predefined theorems. Experts in formal verification and cryptography were continuously involved in design decisions such as what to prove and what assumptions to adopt. The team explains that it kept the portion needing focused human review to about 1% of the entire codebase. But that limited portion includes the specification and trusted base that determine the validity of the proofs, so the small amount of work does not make it any less important.

{
  "type": "bar",
  "title": "Scale of the verification target and proof artifacts",
  "unit": "Lines / instructions",
  "categories": [
    "Binary instructions (AArch64)",
    "Trusted base (TCB)",
    "AI-generated proof code"
  ],
  "series": [
    {
      "name": "Scale",
      "values": [140000, 26000, 6500000]
    }
  ],
  "caption": "The target binary has about 140,000 instructions, the main trusted base is about 26,000 lines, and the AI-generated Lean proof code is about 6.5 million lines. Instruction counts and lines of code are different metrics and are not a direct comparison of workload.",
  "source": "Google DeepMind technical documentation"
}

For roughly 140,000 machine instructions, about 6.5 million lines of Lean proof code were generated. Being able to build a proof of this size automatically is an important achievement, but details of the total computing resources invested, the number of tokens the model consumed, and the monetary cost have not been disclosed. Because the target code, the verification scope, and the maturity of the automation tools differ between traditional manual verification and this experiment, it is hard to judge the degree of productivity improvement from a simple comparison of elapsed time.

Given that five experts worked full time while running agents continuously, that the verification target was confined to a specific binary of about 140,000 instructions, and that no rigorous measured figures for manual verification as a point of comparison have been published, the four-week record does not show that an ordinary company could obtain the same result in the same period. It is more appropriate to regard it as an experimental result showing that AI-agent-based formal verification may make it possible to take on work that previously required enormous human resources. If it can later be shown that other codebases can be verified in a similar period and at practical cost, it will become possible to judge more concretely whether the approach can be introduced into general development processes.

The research team also ran experiments to confirm that AlphaProof Code does not unconditionally prove a faulty program secure. Specifically, it reintroduced two vulnerabilities that Cheval and colleagues had previously found in libsignal and that had already been fixed, by reverting them to their pre-fix state. This is mutation testing: using programs into which known flaws have been deliberately added, it checks whether the verification system can detect the problems.

The first is the "Weak-state" mutant binary, which reverts the fix in commit cd36118, where there was a problem in session-state update handling. The second is the "Small-subgroup" mutant binary, which reverts the fix in commit 5293caa, where inputs belonging to a small subgroup were not properly rejected in elliptic-curve cryptography operations. Both were changes made to reproduce actual flaws confirmed in the past.

When the team recompiled these mutant binaries and fed them to AlphaProof Code, the system did not produce a false proof that security held. Instead, it constructed concrete inputs that contradict the symbolic security theorems and, according to the team, mechanically proved in Lean that the target binaries do not satisfy the security conditions. This means that, at least for the two known flaws selected here, AlphaProof Code was able to detect the security violations.

This result cannot, however, be interpreted as proof of an ability to find every unknown vulnerability. What was tested was the ability to detect two specific flaws, and it has not been shown that the system can comprehensively find attack methods or vulnerabilities outside its scope. The range that formal verification can guarantee is determined solely by the defined specification and attacker model. This point is also important for distinguishing AlphaProof Code from a general vulnerability scanner.

The research output is public, but this is not a verification service for general use

To coincide with the announcement, DeepMind released the formal verification artifacts as open source in the google-deepmind/code-verification repository on GitHub. The published materials include the machine-code model extracted from the compiled binary, the roughly 26,000-line trusted base, and a set of theorem files that can be mechanically checked in Lean. This allows outside security researchers and formal verification experts to independently examine the published proofs and their preconditions. Publishing the artifacts is nonetheless a separate matter from third parties having reproduced the same verification results, which makes future independent verification important.

This release should also not be confused with general availability of AlphaProof Code itself. According to a report by Axios in the US, AlphaProof Code is currently positioned as a cutting-edge research project rather than a cybersecurity product intended for commercial rollout. What has been published is mainly research results and verification materials; no product has been offered that lets ordinary developers input arbitrary software and run the same verification.

There are also constraints on access to Gemini 4 Carbon, which was central to proof generation. The model, announced by Google on October 28, 2026, is being rolled out in stages to defensive security organizations and some trusted partners. An environment in which ordinary developers can combine it with AlphaProof Code and freely run formal verification of their own products through an API is not currently in place.

In its official explanation, DeepMind cites areas requiring especially high reliability, such as medical device firmware and power-grid control software, as future applications. It also outlined prospects for cooperation with its automated vulnerability-fixing agent CodeMender and the security research team Project Zero. These are, however, directions for future research and development, and they do not mean that verification of actual critical infrastructure has been completed or that a mechanism integrating automatic fixing and formal verification has been put into practical use.

From the standpoint of adoption in corporate development settings, several challenges remain. Access to the models needed for verification is limited, the computing resources and costs required for proof generation are unknown, and drafting specifications and establishing a trusted base when applying the approach to different software also require specialized expertise. At this stage, AlphaProof Code is therefore best seen not as a security-checking tool that can be dropped straight into existing development pipelines, but as a research result showing the potential of AI-driven formal verification and as reference material for thinking about future verification methods.

What matters most about this result is that it demonstrates a concrete division of labor for verifying compiled machine code: humans define the security requirements, LLM agents build the vast proofs, and Lean's verification kernel confirms mathematical correctness. A structure in which humans do not simply trust AI-generated code or explanations but confirm correctness through formal verification has important implications for software development that demands high reliability.

Still, what AlphaProof Code proved is not the absolute security of the Signal protocol. It is a conditional mathematical fact: under specific cryptographic assumptions and an execution environment, the machine-code binary under verification satisfies the defined security properties. Behind that guarantee lie the roughly 26,000-line main trusted base audited by humans and additional assumptions about the proof system and execution environment. Whether this method spreads as a practical verification technology will depend on whether third parties can reproduce the proofs, whether it can be applied to other cryptographic libraries and real systems, and whether it is economically viable once the required computing resources and expert effort are included.