Abstract

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. AlphaProof Code consists of a human-guided agent for writing Lean specifications of code, a formal semantics of AArch64 machine code, and a team of autonomous prover agents whose proofs are accepted only if Lean’s kernel checks them against the approved specification. Applied to libsignal, our agents generated about 6.5 million lines of machine-checked Lean proof code, resting on about 26,000 lines of trusted specifications and AArch64 semantics. The proofs cover Signal’s post-quantum PQXDH handshake and Triple Ratchet, establishing forward secrecy, authentication, post-compromise security, and handshake secrecy. They are the first proofs connecting protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation. The results suggest that AI can make formal verification, historically too expensive for most software, practical for real-world systems. Our Lean development is available at https://google-deepmind.github.io/code-verification.

1 Introduction

Ensuring that the software that powers our world is correct and secure is one of the longest-standing challenges in computing [98]. Today, assurance primarily comes from testing, bug finding, and code review. However, reactive bug finding has inherent limitations, even when applying advanced AI systems for cyber-defense [29, 10, 77] to find and fix bugs quickly. An alternative is formal verification [54, 60, 61], where one specifies the correctness and security properties that a software system must enforce and then mathematically proves that the system satisfies them. Such a proof rules out every bug or attack that would violate those properties.

For all of its potential benefits, formal verification is notoriously difficult. While there have been heroic efforts to verify important, complex systems, they come at a high cost. The formally verified seL4 microkernel—perhaps the biggest success story in the field—took twenty person-years to verify [66]; the CompCert verified C compiler [73] took six. Further, in these successful examples, the source code of the system was written specifically with verification in mind. Verification of pre-existing industrial-strength code, such as a production library as compiled by an optimizing compiler, is even harder, as the prover cannot modify the code to make the proof simpler. Such labor costs are untenable for all but the most mission-critical domains.

In this paper, we show that recent AI advances can drastically reduce these costs. We present AlphaProof Code (Figure 1), a framework in which a human user and AI agents collaboratively write Lean [45] specifications of real-world code, and, once the user has vetted a specification, a team of autonomous agents proves that the code satisfies it. We used the framework to verify key security properties of libsignal, the reference implementation of the Signal protocol [91, 74], at the machine-code level. Our results are a significant milestone towards a grand challenge launched in April 2026 [23], and achieving them would have required years of expert labor with earlier tools.

Signal (§3) is the de facto global standard for end-to-end encrypted messaging. It protects the communications of billions of people worldwide: in addition to the standalone Signal application, variants of the protocol are deployed in WhatsApp, Meta’s Messenger app, and Google Messages. The protocol includes sophisticated components such as the PQXDH handshake [69] and the Triple Ratchet [48], which are designed to ensure the security of messages even when some of the keys are compromised, and even against future adversaries with access to a quantum computer.

There is a long line of work on formal security verification of cryptographic protocols [49, 31, 17, 86, 15], including Signal [43, 28, 52, 40]. However, all of these efforts target abstract protocol models, verification-friendly reimplementations, implementations modified to simplify verification, or narrower properties such as crash-freedom (§8). By contrast, we give the first proofs of protocol-level security properties for a widely deployed, unmodified implementation of a cryptographic protocol. More generally, our work shows that AI can verify machine code against rich specifications from the research literature, including properties of the interaction between a stateful program and an adaptive adversary.

We link libsignal into a small command-line harness and compile it with the stock rustc compiler to AArch64 Linux machine code, with low-level cryptographic primitives specified by contracts (§4). We use AlphaProof Code to verify the code’s security in the two standard models of protocol security: the symbolic model (aka the Dolev–Yao model) [49], which treats those cryptographic primitives as abstract “black boxes” achieving standard security properties, and the computational model [56], which bounds an efficient attacker’s success probability by the hardness of the underlying primitives.

Our specification-writing agents start with established symbolic [40, 28] and computational [7, 52] specifications for Signal and adapt them to Lean. However, the existing specifications do not take us all the way, as they analyze the handshake and the ratchet separately and predate Signal’s post-quantum ratchet. With human guidance, our agents extend these specifications to the protocol as deployed. Our agent-written proofs of these specifications establish forward secrecy, post-compromise security, and message confidentiality and authenticity directly for the compiled binary (Table 1, §5.1, §5.2), against classical attackers, and, in the symbolic model, handshake secrecy against a future quantum attacker.

Our proofs amount to about 6.5 million lines of Lean. The statements and definitions a reader must read and trust are about 18,000 lines of code in our repository, plus about 8,000 lines of the AArch64 semantics and the symbol names in a Lean representation of the compiled machine code, whose bytes Lean checks against the executable. To check that our specifications catch real mistakes, we re-introduced two previously fixed libsignal bugs [40] and proved in Lean that the resulting binaries violate our symbolic security theorems (§6). Our Lean development, with all specifications and proofs, is available at the website https://google-deepmind.github.io/code-verification.

2 AlphaProof Code

AlphaProof Code (Figure 1) is a framework for human–AI collaboration on the formal specification and verification of real-world software. The framework is based on a simple principle: The majority of human effort in software verification now lies in engineering the specification, the formal statement that is proved and its assumptions about how the machine code executes. Previously, the expertise and labor required to write proofs was a bottleneck to large-scale formal verification, but this is no longer the case. As we demonstrate, even large proofs about software can be written by teams of AI agents once a specification is fixed, and the proof agents can work autonomously: since the proof is ultimately checked by the Lean kernel, the reliability of the results does not depend on the reliability of these proving agents.

For large, complex systems, AI assistance can reduce the cost of specification writing and assurance but not completely replace human judgment and review. Based on these observations, we propose that human authors select what to prove, resolve ambiguities, evaluate security trade-offs, and make all final decisions, while AI agents draft and test specifications under human direction.

We now describe the four components of AlphaProof Code (Figure 1) in turn.

2.1 Specification Writing

A specification in AlphaProof Code consists of a set of Lean theorem statements together with every definition they depend on, such as models of the code’s environment. The specification defines what correctness and security mean for the program, and what classes of bugs and attacks the proof excludes. The specification must be trusted, meaning that the validity of the final result depends on getting it right, and it cannot be automatically checked—a flaw could weaken the guarantee the theorem provides (shaded in Figure 1). By contrast, the multi-million-line proofs produced by AI agents are untrusted: any logical error in a proof is rejected by Lean’s kernel, preventing the proof from going through. The trusted definitions and theorem statements in the specification build on knowledge available in research papers and standards. The definitions can also include extern contracts that define assumptions about parts of the system that are outside the scope of the verification campaign. For the Signal proofs, the trusted computing base is described in §5.3.

All agents in AlphaProof Code, including the specification writer, are general-purpose coding agents whose behavior is defined by skills: natural-language documents that describe an agent’s task, the sources it should consult and the checks it must perform. The specification-writer agent drafts trusted theorems and definitions under close guidance from the user. A pool of reviewer agents checks that a draft is faithful to its sources and to the implementation.

Even when a model from the literature exists, it can take many rounds of iteration between the user and the agents to arrive at a good specification. For instance, prior formal models of Signal analyzed its initial handshake and its ratchet separately. Our specifications had to compose these models and cover Signal’s new post-quantum ratchet (§5.1, §5.2), and this took several rounds of drafts and review. The user reviews, revises, and approves the specification before any proofs are written, and its git commit becomes the baseline that the gatekeeper later checks proofs against.

Much of this iteration is designed to ensure the specification’s strength. A theorem that makes overly restrictive assumptions on the inputs, asserts only weak properties of the output, or places too few constraints on existentially quantified witnesses can hold even for buggy code. For instance, the computational security proof states that there exists a reduction from an attack on the protocol to a violation on an underlying assumption (§5.2.2). If a mistake in the specification weakens the capability of the attacker, then the security guarantee is also weakened. This is the sort of mistake that the iteration is designed to prevent.

For this reason, we use several techniques to test the specifications and assure their quality. Human authors review the specification; even so, specifications are like any large software artifact, in that human review is not expected to detect all bugs in a large codebase. Therefore, AlphaProof Code also includes several means of automated testing. First, reviewer agents are asked to provide reviews from a skeptical perspective, and in our experience were effective at detecting soundness and strength issues in the specification. Second, the prover agents create theorems to check the specification’s quality, which are formally proved. For example, contradictory hypotheses make a theorem vacuous, so the agents also prove that the hypotheses are jointly satisfiable and that the theorems’ premises are met by concrete executions, in the spirit of vacuity detection in model checking [20, 70]. Third, mutation testing in software engineering is a well-known technique for evaluating the effectiveness of test suites by injecting artificial mistakes into the code and seeing if the test suite fails [47, 64]. To test specifications this way, agents add natural bugs to the code, such as skipping the ciphertext MAC verification in Signal, and prove that the security theorem is false when applied to this mutated binary. Finally, we check that the specifications would have prohibited historical bugs in the system (§6), again in the sense that the symbolic security theorem is provably false.

2.2 Machine-Code Semantics

Our theorems are stated over a formal semantics of user-mode AArch64 Linux, written in Lean. The semantics takes an executable (an ELF binary) as a list of bytes and describes all of its possible runs as a relation between inputs, such as command-line arguments, standard input and the initial file-system state, and outcomes, such as the exit code, standard output and the final file-system state. The central definition, ElfRunsTo bin pre post, states that every run of bin from inputs satisfying pre ends in an outcome satisfying post, and that no run faults, for instance by reading unmapped memory. For the theorems to apply to real executions, the semantics must be sound: every behavior of the real hardware and kernel must be a possible run of the semantics. This cannot be proved, since the hardware and kernel are not formal objects. Consequently, our approach is to keep the trusted definitions small and test them extensively.

The semantics models a single-threaded, statically linked process. A machine state holds the general-purpose and SIMD/floating-point registers, the program counter, the condition flags, a byte-addressed memory with per-page permissions, and the files in the current directory. A decoder turns the bytes at the program counter into an instruction, and the effect of each instruction follows Arm’s machine-readable ASL specification [12, 13, 84]. Because code and data share one memory, writes to executable memory, accesses to unmapped memory and permission violations are faults, so a proof that a run terminates normally rules them out. Above the instruction level, a loader parses the ELF file, maps its segments and builds the initial stack, as Linux does when it starts a process. System calls are interpreted by a model of the calls the program uses: memory management, file and stream I/O, and exit. A run ends in one of two ways: it exits with an exit code, or it exits abnormally and faults due to an error, a panic, or an unmodeled instruction or system call. The semantics covers 467 instructions and 31 system calls in 7,578 lines of Lean. It does not model threads, signals, the vDSO, dynamic linking, or files outside the current directory, so programs that rely on them cannot be verified.

The trusted parts of the semantics, namely the decoder, instruction semantics, memory model, loader and system-call model, contain only definitions. The program logic used in the proofs is not trusted: its separation-logic rules, weakest-precondition calculus and proof automation are all proved sound in Lean against ElfRunsTo. We validate the trusted definitions by intensive testing. Instruction execution is tested in lockstep against two independent oracles: the Unicorn emulator (whose code is derived from QEMU), and the Sail model of Armv9.4-A [14], derived from Arm’s official specification. The tests include single instructions, published test vectors, random instruction sequences and compiled Rust functions. The loader and the system-call model are tested against qemu-aarch64 on a large number of binaries.

Two features of the semantics matter for specifications. First, the semantics treats the physical memory available to the process as a finite input, and a run that exhausts it ends in an out-of-memory outcome. A theorem then either proves, given a lower bound on available memory, that no run exhausts it, or accounts explicitly for the runs that do (§5.2.4). It is assumed that the operating system provides physical memory if available. Second, a proof can hook a function (linked either from a library or as a four-byte trap stub in the executable): a call to it is intercepted at entry and modeled with a trusted contract instead of executing code. This is how assumptions about cryptographic primitives enter a result, since their security cannot itself be proved, and it is also used for error-message formatting and a few routines such as the functions that write files and standard output. Hooks are part of the specification and are reviewed carefully (§2.1).

2.3 Proof Synthesis

Our proofs are produced autonomously by a team of agents with distinct roles, each defined by a skill. An orchestrator divides up the work and schedules agents but never edits Lean files itself. Each subtask is assigned to a proof worker. The main difficulty in a large team is managing context: each agent’s context window is limited, and state can be lost when the context is compacted. The orchestrator therefore groups workers under team leads, each responsible for a larger, longer-running goal. A lead absorbs the back-and-forth with its workers and sends the orchestrator short summaries of open obligations, completed lemmas and blockers. Agents also try to falsify a goal before work on it starts, to avoid wasting resources on unprovable subgoals.

A few fixed roles keep the shared codebase coherent as the proofs grow. An architect designs, and periodically revises, the high-level decomposition of the proof. An integrator merges verified proofs into library modules, removes duplicate lemmas and generalizes lemmas for reuse. To avoid conflicts among dozens of concurrent agents, each file is edited by at most one worker at a time, and only the integrator commits to the repository. Other support roles schedule expensive Lean builds and monitor agents and resources. In our proof campaigns, a team typically had 40 to 80 agents and ran on a single machine for 24 to 72 hours.

Proof attempts can reveal that a specification is subtly wrong about the code or its environment. Agents cannot edit the specification, but they can propose an amendment to a critic agent, which never sees the proof attempts. The critic accepts an amendment only if three conditions hold. First, the amendment must be necessary, as shown by a machine-checked disproof, a counterexample on the binary or an argument grounded in the code. Second, it must not weaken security, and any assumption it adds must hold of the real code. Third, it must be small, typically a few lines in one definition. Amendments that change trusted assumptions are approved by the user or under a user-set policy, and each is logged with its justification. Examples from our campaign include amendments that strengthen trusted contracts for library functions to match their real behavior, for example, “memcpy may copy from read-only memory.”

2.4 Gatekeeping

A proof is accepted only if it proves exactly the statements the user approved. Inspecting the theorem statement alone is not enough to check this, since a statement can be weakened indirectly by changing a definition it depends on. The gatekeeper is an agent used during development to check recorded approvals for specification amendments (if any) and to call the standard comparator tool [72] to check the proof.

The agent invokes comparator using a deterministic script that can be rerun manually when desired. We keep a strict discipline of which files are in the trusted specification of the theorem versus the untrusted proof, enforced by deterministic scripts, which allows clean rerunning of comparator. At the start of a campaign, the gatekeeper copies the specification from the baseline commit into a held-out directory that no agent can write to. The held-out copy changes only through accepted amendments (§2.3), which are reviewed by the critic and approved by human authors before the gatekeeper applies them.

The gatekeeper accepts a proof only if comparator confirms that the statement and every definition it depends on are identical to this copy, that the proof uses only Lean’s standard axioms, and that Lean’s kernel accepts the proof. At that point, the gatekeeper declares that the proof is complete (proof agents, team leads, and the orchestrator cannot declare a top-level goal done on their own). When proof development is complete, we re-run comparator manually for further assurance.

3 Background on Signal

Signal is a protocol for asynchronous messaging, meaning that it allows a user Alice to start a conversation with a user Bob and send him messages while he is offline. A server stores and relays messages but is not trusted for either confidentiality or authenticity. We describe the version implemented by libsignal v0.105.4, restricted to one-to-one sessions. (We leave group messaging as future work.) A session has two phases (Figure 2): a handshake, in which Alice and Bob agree on a shared secret, and a ratchet, which derives a fresh key from that secret for every message.

The handshake relies on Diffie-Hellman (DH) key agreement: Alice combines her private key with Bob’s public key, Bob does the reverse, and both get the same value, which an eavesdropper cannot compute from the public keys alone. Since Bob may be offline, he leaves public keys, called prekeys, on the server for senders to use. Signal’s handshake, PQXDH [69], mixes several DH values with a post-quantum key encapsulation mechanism (KEM). The resulting secret survives the leak of some of these keys, and an eavesdropper who records the handshake cannot recover it even with a future quantum computer.

The ratchet, which Signal calls the Triple Ratchet [48], combines the classical Double Ratchet with the Sparse Post-Quantum Ratchet (SPQR) [89]. This design contains the damage from a stolen key. Each message key is derived from the previous state by a one-way function and then deleted; stealing a party’s current state therefore exposes no earlier encrypted messages (forward secrecy). Every reply also mixes in a fresh DH value, which locks out an adversary who stole the state, as long as it stays passive during that fresh DH exchange (post-compromise security).

Our goal is to show that these properties hold against a strong adversary that controls the network and the server and may compromise long-term keys, prekeys or a party’s entire state. For the post-quantum properties, the adversary may later break DH. §5.1 and §5.2 state secrecy, authentication, forward secrecy and post-compromise security precisely.

The subsequent sections of this paper refer to a few more of libsignal’s components. Bob’s prekey bundle holds his long-term X25519 identity key, a signed prekey and a Kyber1024 prekey,¹ both signed with the identity key using XEdDSA, and optionally a one-time prekey that the server hands out only once. On the ratchet side, a root key absorbs the fresh DH values and yields chain keys, from which message keys are derived. SPQR runs a separate ML-KEM-768 exchange and mixes its keys into every message key, so that post-compromise security also holds against a quantum adversary. Appendix A has the full key schedule.

The code does much more than the protocol described above, and this is where implementation bugs arise. For example, libsignal keeps a large mutable session state, stores keys for messages that arrive out of order, splits SPQR’s ML-KEM messages into chunks spread over ordinary messages, and uses protobuf for serialization. It also keeps archived earlier sessions so that delayed messages can still be decrypted. Because our theorems are about the compiled code, they cover this machinery. In one now-fixed bug, a prekey message that decrypted only under an archived session caused libsignal to store the new session’s state anyway, including a copy of the signed prekey’s secret. When we reintroduce it, the resulting binary provably violates our symbolic security theorem (§6).

Table 1 summarizes our verification results for the protocol. More details are available in §5 and the appendix.

4 Setup for Verification

We verify the one-to-one session code of libsignal-protocol (v0.105.4, with spqr v1.6.0): PQXDH session setup and Triple Ratchet messaging. Rather than reasoning about its Rust functions and in-memory state, we wrap the unmodified crates in a small command-line harness, libsignal-cli, and state our theorems about whole runs of its compiled AArch64 executable. Each run of this tool performs one operation for one party specified with command-line arguments: keygen creates the party’s keys, init starts a session from a prekey bundle (process_prekey_bundle), and send and recv encrypt and decrypt one message (message_encrypt, message_decrypt). Our theorems cover init, send and recv; keygen is not verified, and the theorems instead take the parties’ keys as part of their setup.

Call::Init { peer, bundle } => {
    let (me, bundle) = (me?, read_bundle(&bundle, peer.device_id())?);
    let (sessions, identity) = (&mut s.sessions, &mut s.identity);
    accepted(initiate(&peer, &me, sessions, identity, &bundle, now))?;
    Vec::new()
}
Call::Send(peer) => {
    let me = me?;
    let (sessions, identity) = (&mut s.sessions, &mut s.identity);
    let message = accepted(encrypt(input, &peer, &me, sessions, identity, now))?;
    [&[message.message_type() as u8], message.serialize()].concat()
}

ALICE=8a6f1c2e-3b4d-4e5f-9a0b-1c2d3e4f5a6b.1  BOB=5d3e2f10-7a8b-4c9d-8e0f-a1b2c3d4e5f6.1
run()    { head -c 16384 /dev/urandom > $1/coins; (cd $1 && libsignal-cli "${@:2}"); }
bundle() { mkdir $2; cp $1/public/⟨identity key, one prekey of each kind⟩ $2/; }
mkdir alice bob
run bob keygen $BOB 1                            # Bob's keys; public halves in bob/public/
run alice keygen $ALICE 0
bundle bob bob_public_bundle                     # play the server
run alice init $BOB ../bob_public_bundle         # PQXDH
printf "Hi Bob!" | run alice send $BOB > m1      # m1: a PreKeySignalMessage
run bob recv $ALICE < m1                         # prints Hi Bob!
printf "Hi Alice!" | run bob send $ALICE > r1    # r1: a SignalMessage
run alice recv $BOB < r1                         # prints Hi Alice!
run bob recv $ALICE < m1; echo $?                # replay: prints 1; no file written

States. A party’s state is stored in a directory (Figure 3 and Figure 4). Its files hold everything libsignal stores for the party, in libsignal’s own serialization format: its identity key pair, its sessions (one per peer device), its signed, one-time and Kyber1024 prekeys, and the identity keys of its peers. The subdirectory public/ holds what a client uploads to the Signal server: the public halves of its keys and their signatures. Nothing else survives between runs, so leaking a party’s directory is exactly a compromise of its whole state.

Process semantics. A run depends only on its command line, its standard input, the party’s files, and a file coins that supplies all of its randomness; the clock is fixed and no other entropy source is read. A run produces only an exit code, its standard output, and new contents for the party’s files. Exit code 0 means that libsignal accepted the operation: the changed files are written, and the output (a wire message for send, a plaintext for recv) is on standard output. Exit code 1 means that libsignal rejected it, and then no file is written: libsignal updates its stores one at a time and may fail after some have changed, so, like Signal’s own mobile apps, libsignal-cli holds back all store writes until the operation succeeds. (Exit code 2 reports a malformed command line or an unreadable file.) Our theorems speak only about these inputs and outputs, using a Lean model of how Linux loads and runs an AArch64 executable.

Between runs, control passes to the environment (Figure 3). It runs every call of libsignal-cli, holds all of the parties’ files, plays Signal’s server by building each prekey bundle as a directory of copies of the peer’s public/ files, and supplies the coins of every run. The attacker lives inside the environment. It decides which party runs which operation, and when. It controls the network: the environment hands it every wire message that a run writes to its standard output, and it chooses what each run reads on its standard input, so it may drop, reorder, replay or modify messages. When it asks to compromise a party, the environment gives it that party’s files. This picture is common to both of our proofs; they differ in how they formalize the environment and the attacker’s capabilities. In the computational proof, the environment is a security game and the attacker is any probabilistic algorithm that makes a bounded number of queries; the security proof bounds its advantage at telling which of two challenge messages was encrypted or getting a forged message accepted. In the symbolic proof, the runs and the environment’s actions are matched by transitions of the DyLean [99] model of the protocol, a compromise leaks the secrets in the party’s files one at a time, and the attacker is a Dolev–Yao attacker that computes on symbolic terms; security is a property of every trace.

Because libsignal-cli is an ordinary executable, the same scenarios can also be run directly from a shell. The script in Figure 5 plays both the environment and the attacker: it creates Bob and Alice, plays the server to give Alice a bundle of Bob’s keys, runs the PQXDH handshake and two Triple Ratchet messages, and finally, as the attacker, replays Alice’s first message, which Bob rejects without writing any file. We also ran these scenarios on our Lean semantics of the binary (15.6 million instructions across 10 invocations), and every run had the same outcome as on the real binary, including all session state.

Verification target. We compile libsignal-cli and the unmodified libsignal crates with stock rustc (1.98.1) and link them statically with musl using stock LLVM ld.lld into one AArch64 Linux executable (build details in §C.6). The proofs follow each init, send and recv run from the executable’s entry point to its final exit_group system call. The proof must reason instruction by instruction about the CLI and its file-backed stores (including the routines that read files and standard input), musl’s mallocng memory allocator and memcpy/memset, string cloning, the PQXDH, Triple Ratchet and SPQR state machines, key derivation (HKDF and libsignal’s HMAC-SHA256, apart from the hooked SHA-256 compression function), protobuf serialization and MAC verification. The remaining 37 hooked routines are replaced by contracts at the binary boundary, and 18 panic entry points end the run with SIGABRT. The hooked routines are the low-level cryptographic routines (SHA-256 and SHA-512 compression, AES-256-CBC, the X25519 and Edwards curve operations used by XEdDSA, Kyber1024 in PQXDH and ML-KEM-768 and HMAC from libcrux in SPQR); error-message formatting (core::fmt::write and format_inner); three libc memory and string routines (memmove, bcmp and strlen); the two functions that write files and standard output; and the remaining non-crypto Rust library routines not yet de-hooked: UTF-8 checking, memrchr, the fixed clock, an optimization barrier, and the zeroizing destructors of X25519 secrets. In our main theorems, each hooked routine is a fixed Lean function; the cryptographic primitives inside these functions are left abstract. The functional-correctness theorems proved about the binary are shared by the computational and the symbolic security proofs.

The contracts for the cryptographic routines idealize the primitives, since our results are conditional on their security. The remaining contracts describe the routines’ functional behavior. They are not proved against the real routines, but the scenarios of Figure 5 have the same outcomes when run with them in the Lean semantics as on the real binary.

While our setup models a specific execution environment, our results are relevant to many others. For example, the Signal apps for Android and iOS run the same Rust code for libsignal. Nearly all Android phones and all iPhones use AArch64; the difference is in compiler flags, linking, and the operating system interface. The theorems we prove carry over to these other execution environments as long as we trust that they preserve the behavior of the protocol code as exercised by the libsignal-cli binary.

4.1 Binary-Level Guarantees

The security proofs described in this paper build on a set of theorems about the machine code. These theorems are proved once and for all. They hold for every placement of the code and of musl’s allocator in memory that matches the bytes of the executable, and Lean checks that such placements exist. They also hold for every implementation of the hooked routines.

These theorems state that the executable implements the Lean models of libsignal on which the security proofs are built. For example, our computational security theorem (through Lemma 4) states that on every init, send and recv run whose inputs are within the stated size limits, the executable does what the model prescribes. If the model accepts the operation, the run exits with code 0, prints the model’s output, and leaves exactly the model’s new state in the party’s files. If the model rejects it, the run exits with code 1, prints nothing, and leaves every file unchanged. If the model panics, the run ends with SIGABRT. The CLI’s own checks are proved as well: a run exits with code 2 if its standard input exceeds $2^{20}$ bytes, and send rejects plaintexts longer than $10^6$ bytes. In particular, no run faults, loops forever, or leaves a state that the model would not produce. The symbolic refinement proof is built on the same facts.

The only exception these theorems allow is a run that exhausts the machine’s memory. A separate theorem shows that this does not happen: in our process model, which gives each run 1 GiB of memory beyond its loaded segments and an 8 MiB stack, no run on inputs within the limits reaches the out-of-memory state. Its proof bounds the heap use of every run through the verified allocator, using the fact that a session record stays below 1.2 MB however many messages the session carries. The security theorems therefore contain no out-of-memory term, and the symbolic theorem states outright that every valid call exits or aborts and never faults or diverges.

These guarantees concern a fresh process started with only standard input, output and error open, an empty environment, and a fixed clock. The kernel’s random bytes are fixed, so all of a run’s randomness comes from its coins file. The hooked routines are replaced by their contracts. The guarantees say nothing about a machine with less memory, about processes launched with other files open, or about the code of the hooked routines themselves. The security theorems constrain those routines separately.

5 Verifying Signal

We verify the security of the libsignal-cli binary (§4) in two established models from the research literature: the symbolic model (§5.1) and the computational model (§5.2). In the symbolic model, cryptographic primitives are idealized and output abstract terms. The goal is to show that in every possible execution, secret values (e.g., messages) remain secret and parties agree on whom they are talking to. In the computational model, messages are bit strings and the adversary is a probabilistic algorithm that interacts with the protocol through a bounded number of oracle queries. The proof objective is to show that breaking the protocol is at least as hard as breaking the cryptographic primitives it is built from: any adversary’s advantage in attacking the protocol is bounded by a function of the advantages of efficient reductions that break some underlying cryptographic primitive.

We work in two independent models for two reasons. First, we wanted to learn whether agents can carry out proofs in both models, which differ in their tools, their methods of reasoning and the ways they fail. Second, the two proofs give different assurances about the protocol. The computational proof bounds the advantage of any query-bounded adversary and accounts for events, such as collisions, that the symbolic proof abstracts away. The symbolic approach, in turn, follows libsignal’s session records more closely and states ten properties under a richer set of compromises. The symbolic proof also covers an attacker (for example, a future quantum computer) that breaks Diffie–Hellman after the handshake. By contrast, our computational proof only covers classical adversaries.

5.1 Symbolic Proofs

We prove that the libsignal binary enforces symbolic security properties of the composition of PQXDH and the Triple Ratchet, down to the assembly level. The symbolic model of cryptography simplifies verifying the high-level design of cryptographic protocols by assuming the underlying primitives obey “ideal cryptography” (e.g., no hash collisions, encrypted values are meaningless to attackers without the key). This enables a separation of concerns: developers of the underlying primitives can validate these standard assumptions, while a symbolic analysis of a protocol can rely on them to prove protocol-specific properties.

Most symbolic security verification efforts verify abstract designs and give no assurance about the real implementation. We instead define and prove symbolic security properties of the compiled binary using the following approach:

1. Symbolic Model. We use DyLean [99], an existing Lean framework for symbolic cryptography, to write one composed model of PQXDH and the Triple Ratchet (§5.1.1).

2. Security Theorems. We state and prove that the model satisfies ten security properties, replicating the symbolic state-of-the-art for Signal [40, 28] (§5.1.2).

3. Assembly-level Symbolic Events. To state symbolic security at the binary level, a thin trusted event layer turns executions of the binary under our AArch64 semantics into hardware traces of protocol events: one event per run of libsignal-cli, and one per leak, break or inversion by the attacker between runs (§5.1.3).

4. Refinement. We prove that every hardware trace is explained by a model trace, up to collisions. A trusted concretization function $\gamma$ gives the bytes that each model term stands for (§5.1.4).

5. Preservation. We prove that refinement and the model-level theorems together imply the same ten properties, for an attacker that knows only what it observed of the execution, on every hardware trace whose coins never repeat a secret: on the whole trace if it is collision-free, and otherwise on its explained prefix before the collision (i.e., our refinement definition preserves symbolic security; Theorem 1, §5.1.5).

The first three items comprise the trusted definitions (§5.3); everything that connects them (the model-level proofs, refinement and preservation) is proved in Lean.

Figure 6 shows an overview of this approach. Steps 1 and 2 follow prior work closely. The challenges are in steps 3 and 4, because the binary does not satisfy the symbolic assumptions. First, hardware has no messages: the CPU only reads and writes registers and memory. We address this with a small, trusted augmented program semantics that primarily calls our AArch64 one, but extends it with these events as described in §5.1.3. Second, hardware values are finite byte strings, not terms. A Dolev–Yao attacker cannot guess a key, but an attacker of the binary can guess libsignal’s 8-byte MAC with probability $2^{-64}$, so the binary does not refine the model exactly. Following Arquint et al. [15], §5.1.4 maps model terms to bytes but never maps bytes back to terms. A guessed value is then a different term whose bytes happen to collide.

Crucially, we do not aim to advance the state of the art in what has been proven about the Signal protocol [74, 91] at the symbolic level. Our contribution is replicating the state of the art at the symbolic level and rigorously connecting it to the assembly implementation for the first time.

5.1.1 Symbolic Model

DyLean [99] is a Lean framework for symbolic protocol analysis in the style of ProVerif [33] and Tamarin [76]. A protocol is a labeled transition system that produces atomic transitions over a global append-only trace. The transitions are scheduled by the (Dolev–Yao) attacker, who also chooses their inputs. Security theorems are described in terms of the attacker’s knowledge of a trace, which is the least set of terms that contains everything the trace reveals (its network messages, including leaked secrets) and is closed under attacker operations of each primitive. The attacker may inject only terms it knows, so it cannot guess a key or forge a signature.

Attacker operations and symbolic assumptions are both modeled through equational theories, which model the underlying primitives through trusted (assumed) rewrite rules. For instance, dh sorts its two secret exponents, so dh(dhPk(a), b) and dh(dhPk(b), a) are the same term, and symDec k iv c returns m exactly when c is symEnc k iv m and fails otherwise.

The composed model. Using DyLean, we formalize a single composed symbolic model of the deployed protocol by combining the PQXDH handshake model of Bhargavan et al. [28] with the Triple Ratchet model of Cheval, Jacomme, and Richards [40]. Because the binary must refine it, the model is more faithful to libsignal than the papers’ models in two places: it models X25519’s non-canonical encodings and small subgroup, which are outside the scope of Cheval et al.’s proofs and are the setting of the small-subgroup bug of §6; and it models libsignal’s binding of the KEM public key into the shared secret, rather than the change to the associated data (PQXDH Revision 2) that Bhargavan et al.’s ProVerif proofs assume.

The composed model is a labeled state machine covering initial prekey bundle processing (with signed and one-time X25519 prekeys and reusable, last-resort Kyber prekeys; one-time Kyber prekeys are not modeled), prekey message reception, and subsequent Triple Ratchet messaging (the Double Ratchet coupled with SPQR), with unboundedly many sessions but at most one active session per party and role, scheduled by a Dolev–Yao attacker that controls the network and may compromise long-term keys, prekeys, or stored session state. Following Bhargavan et al. [28], the attacker may also break DH (say, with a quantum computer) or KEM (say, with cryptanalysis) and from then on invert public keys of the broken primitive to learn their secrets. §B.1 describes the model as a transition system.

5.1.2 Security Theorems

Table 2 lists the theorems we prove. They restate the forward secrecy and post-compromise security properties that Cheval et al. [40] prove for the Double Ratchet after PQXDH, and the PQXDH theorems of Bhargavan et al. [28]; both papers use ProVerif [33]. All of them hold on every reachable trace of the composed model described above. Neither paper analyzes exactly this protocol, so the last column of the table gives the design-level differences between each paper’s statement and ours. We use libsignal’s names and roles: Alice processes Bob’s prekey bundle and sends the first message, so she is the initiator and Bob the responder. The PQXDH paper swaps the two labels: our initiator secrecy is its responder secrecy (Theorem 7), and our responder secrecy its initiator secrecy (Theorem 9).

Most of the differences are forced by verifying the deployed code rather than a protocol description: libsignal’s three handshake outputs instead of a single key, KEM public-key binding in the shared secret instead of the associated data, and agreement on prekeys only up to re-encoding. To rule out vacuous theorems, we also prove that honest sessions with and without a one-time prekey are reachable, and that the premises of the forward secrecy and handshake secrecy theorems can be met. At the binary level, we prove that the initial setup and four example interactions (handshakes with and without a one-time prekey, an honest session, and one with a leaked key) arise from runs of any implementation that meets the CLI’s functional specification, and that these runs meet every hypothesis of Theorem 1 without a collision.

5.1.3 Assembly-Layer Events

To state security at the assembly level, we add protocol events as a thin, trusted layer on top of the unchanged AArch64 semantics. Protocol-level events are naturally observed at the process interface of libsignal-cli (§4): its command line, standard streams and files already fix which bytes are a plaintext, a wire message or randomness, so no event needs instrumentation inside the binary. A hardware trace is a list of events. Each records either one run of libsignal-cli (init, send or recv) as the environment sees it, or an action of the attacker between runs: leaking a secret from a party’s directory, compromising a party’s DH or KEM, or inverting a public key of an honest party after the matching compromise. The environment may also delete a party’s session file between runs; this emits no event and is how Alice starts a new session. §B.2 lists every event (Table 4).

5.1.4 Refinement

Refinement relates hardware traces to traces of the DyLean model. It rests on a concretization function $\gamma$, which, following Arquint et al. [15, §4.2], maps each model term to the byte string it stands for. Because different terms (e.g., a guessed MAC and the real one) can have the same bytes, $\gamma$ has no inverse, and bytes are never mapped back to terms. $\gamma$ is a homomorphism: each function symbol of the model comes with a function on byte strings, such as libsignal’s protobuf encoding for wire messages. The cryptographic symbols use an interpretation $\mathcal{I}$, which is universally quantified. The only laws assumed of it are a few trusted facts, chosen so that $\gamma$ agrees with the equational theory: algebraic and length facts such as Diffie-Hellman commutativity, canonical X25519 public keys, rejection of public keys shifted by a torsion point, and that every AES-CBC ciphertext that decrypts is the encryption of its plaintext. Two further parameters complete $\gamma$: byte functions $S$ for opaque symbols (SPQR, XEdDSA, Kyber1024 public keys, and decapsulation of non-honest ciphertexts), constrained only to agree with the setup’s provisioned bytes, and a per-trace ghost $g$ giving the bytes of each fresh value and of the wire messages’ addresses field, which the model does not represent (§B.3).

A model trace explains a hardware trace $\tau$ if it is reachable in the model, its events line up with those of $\tau$ one to one, in order, with each byte field of a hardware event equal to $\gamma$ of the corresponding model terms, and it agrees with the execution on details that $\tau$ does not record, such as how stored session records replace earlier ones (§B.4).

Refinement definition. The standard refinement definition would be trace inclusion: every hardware trace is explained by some model trace. That is false here, because hardware bytes are finite. libsignal truncates its MAC to 8 bytes, so an attacker who guesses the MAC makes the binary accept a forged message. In the model, the receiver accepts only if the received MAC term is the one it computes, and a guessed literal is a different term, so no model trace explains that hardware trace. Our refinement definition is therefore trace inclusion up to collisions, stated in full as follows.

For every choice $W$ of the abstract primitives inside the hooked routines, every interpretation $\mathcal{I}$ of the cryptographic symbols that meets their contracts and agrees with $W$, and every well-formed setup $r$ (the parties and their provisioned keys):

Here $S$ gives the opaque symbols’ bytes; $\mathrm{Traces}_{\mathcal{I},W}(r)$ is the set of hardware traces of the binary from setup $r$, with the hooked routines computed from $W$, inversions restricted as in §5.1.3, and the environment restricted as in §B.7; $g$ is a ghost and $\mathit{ms}$ a model trace; and $\gamma_{\mathcal{I},S,g}$ is $\gamma$ with these three parameters fixed. $\mathrm{Collision}(\tau)$ says that a prefix of $\tau$ is explained, and the next run can be explained only through a collision, consisting of two different terms with equal bytes, where at least one term was built by a symbol assumed injective (a fresh value, dhPk, dh, kdfExtract, symEnc, trunc8, or KEM encapsulation).

Typical collision cases are a received message that the binary accepts only because its MAC equals the expected one, and a plaintext equal to a secret the attacker does not know. Read the other way around, every hardware trace without a collision is explained by a model trace.

The collision case is constrained: $S$ is chosen before the hardware trace, a received message counts as a collision only if it collides under every explanation of the prefix that has not already read a colliding message, and never if a term the attacker knows explains it without itself colliding. It also excuses a Kyber decapsulation that disagrees with encapsulation, since no Kyber correctness law is assumed on $\mathcal{I}$. This clause depends only on the hooked Kyber routines, Bob’s provisioned Kyber key and the received ciphertext, so it holds only if decapsulation under that key disagrees with encapsulation: the Kyber implementation is incorrect, the provisioned key is malformed (key generation is not verified), or the ciphertext is one of the decryption failures that Kyber1024 has with negligible probability (§B.5). Bounding the probability of $\mathrm{Collision}$ is a computational question, outside Lean. Arquint et al. instead assume collision freedom as a hypothesis [15, §4.3].

5.1.5 Main Theorem

Our main symbolic result is that every hardware trace of libsignal-cli that does not reach a collision is explained by some model trace, and that all ten theorems of Table 2 hold on every model trace that explains it, against an attacker that knows only what it observed in the hardware trace.

To state it, let $Q(\mathit{tr},K)$ be the conjunction of the queries of the theorems of Table 2 on model trace $\mathit{tr}$ with attacker knowledge $K$. The model-level theorems together state $\mathrm{Sec}(\mathit{Model})$: $Q(\mathit{tr}, \mathrm{Knows}(\mathit{tr}))$ for every reachable model trace $\mathit{tr}$, where $\mathrm{Knows}$ is the attacker knowledge of §5.1.1. The binary-level property $\mathrm{Sec}(\mathit{Asm})$, where $\mathit{Asm}$ is the machine code of libsignal-cli, is the statement of the following theorem.

Theorem 1 (Binary symbolic security). Lean: signal_session_secure_placed For every choice $W$ of the abstract primitives inside the hooked routines, every interpretation $\mathcal{I}$ of the cryptographic symbols that meets their contracts and agrees with $W$, and every well-formed setup $r$ (two honest parties, initiator Alice and responder Bob, their provisioned keys, and each party’s pinned copy of the other’s identity key),

where $\mathrm{Safe}(\tau) := \forall (g, \mathit{ms}) \in \mathrm{Expl}(\tau).\ Q(\mathit{ms}, K_{\mathit{ms}})$.

$\mathrm{Expl}(\tau)$ is the set of pairs $(g, \mathit{ms})$ such that $\mathit{ms}$ explains $\tau$ under $\gamma_{\mathcal{I},S,g}$; requiring it to be nonempty stops the $\forall$ from holding vacuously. $\mathrm{Collision}_{\mathcal{I},S}(\tau_1, e)$ says that $\tau_1$ is explained and that the next run $e$ can be explained only through a collision, as in §5.1.4. A trace has fresh coins if the setup’s X25519 secrets and the secrets that its successful runs draw from their coins (X25519 keys and Kyber encapsulation randomness) are pairwise distinct, compared after X25519 clamping. The theorem also establishes progress: every reachable valid call exits or aborts, and never faults or diverges. The theorem differs from $\mathrm{Sec}(\mathit{Model})$ in four ways. First, a trace that reaches a collision gets the guarantee only on its explained prefix before the colliding run. Second, the knowledge $K_{\mathit{ms}}$ is the same Dolev–Yao closure, but seeded only with the setup’s public values and the terms matched with what the attacker observed: the bundles, the wire messages, and the leaked or inverted secrets. Third, the hardware traces fix a narrower scenario than the model (§5.1.6). Fourth, the theorem assumes fresh coins; if the coins come from a CSPRNG, this fails with probability about $k^2/2^{251}$ over $k$ draws.

Proof sketch. Lean: comp_refinement_preservation_cli The proof is mostly a standard refinement-preservation argument:

where $\mathit{Asm}\sqsubseteq \mathit{Model}$ is the refinement definition of §5.1.4. Every model trace that explains a hardware trace is reachable, so the model-level theorems hold on it, and the hardware attacker knows no more than the model attacker on that trace. Since each query uses the attacker’s knowledge only as a hypothesis, an attacker that knows less cannot break it. In the collision case, the same argument gives the queries on every explanation of the prefix before the colliding run (§B.8).

5.1.6 Limitations

Cryptography. Our guarantees are symbolic: they assume perfect cryptography and say nothing about the computational secrecy of bytes. At the binary level, the theorem excuses byte collisions but does not bound their probability, and it trusts the hooked routines of §4 to meet their contracts and the low-level cryptographic ones to compute an interpretation that satisfies a few algebraic laws. It also assumes fresh coins (§5.1.5). Since no Kyber correctness law is assumed, a run where decapsulation under Bob’s provisioned key disagrees with encapsulation falls under the collision clause and gets no guarantee; this requires an incorrect Kyber implementation, a malformed provisioned key, or a decryption failure that occurs for Kyber1024 with negligible probability (§5.1.4, §B.5).

Scenario. The assembly-level theorem covers a narrower scenario than the model (§B.7 lists its main restrictions). XEdDSA and SPQR are opaque in $\gamma$, so we assume an authentic PKI and SPQR fields copied from honest messages: both parties start with each other’s identity key pinned, so libsignal’s trust-on-first-use path is not exercised, and the bundle Alice receives carries Bob’s genuine identity key, signed prekey and Kyber prekey. The harness provisions two honest parties with fixed roles and one session per session file, and gives Bob one signed prekey, one reusable last-resort Kyber prekey and at most one one-time prekey; one-time Kyber prekeys are not covered. It also bounds input sizes and the number of sends, requires coins files of exactly 192, 64 and 32 bytes for init, send and recv, and restricts Bob after a non-matching prekey message. A run that aborts (for instance on a failed allocation) ends the trace.

Attacker. Leaks reveal only long-term and prekey secrets and the keys of a party’s current session; side channels and other secrets in memory are out of scope. An exact replay of a prekey message counts as the same session in the model, so our forward secrecy and post-compromise security theorems do not rule out the replay-based loss of forward secrecy described by Cheval et al. [40, §3.2.2–3.2.3]: the binary runs libsignal’s deduplication of base keys, but the model does not require it.

Relation to prior analyses. We replicate only the symbolic results of the papers: the computational theorems of Bhargavan et al. have no counterpart here (see §5.2.3 for our computational guarantees), and we do not model header encryption, which libsignal does not use. Finally, as in Cheval et al., our ratchet theorems let the attacker choose the SPQR keys, so they show that the Triple Ratchet is no weaker than the Double Ratchet, not the post-quantum healing that SPQR adds. In particular, once DH is broken, at any point in the trace, the ratchet’s DH secrets count as compromised, so post-compromise security claims no healing against an attacker who can break DH, even one who cannot break the KEM.

5.2 Computational Proofs

We state computational security as a game [88, 22] between a challenger and an adversary. The challenger samples the secrets and holds every party’s state, and the adversary interacts with it through oracles that run protocol steps, corrupt parties and pose challenges. The adversary’s advantage measures how well it does in violating some security property, for example, its probability of getting a forgery accepted, or its probability of guessing a hidden random bit (minus the trivial 1/2 probability of blindly guessing). If the probability of guessing a hidden bit is, say, $1/2 + 2^{-64}$, we conclude that the bit is effectively secret.

Security is proved via reductions. A reduction $R$ to an assumption, such as the hardness of Gap Diffie-Hellman (Gap-DH), is an algorithm that uses the adversary $A$ as a subroutine to violate the assumption. $R$ runs $A$, answers $A$’s oracle queries itself so that $A$ appears to be attacking the protocol, and turns $A$’s advantage into a solution of its own challenge (say, a challenge instance of Gap-DH). A proof shows that the advantage of $A$ in attacking the protocol is bounded by some function of the corresponding advantage of various reductions $R$ in violating different assumptions, and statistical terms (such as the probability of a collision). If every hardness assumption holds then all reductions have small advantage and we infer that $A$ has small advantage in breaking the protocol. Importantly, the reductions must be efficient for the claimed bounds to be meaningful.

Proofs usually proceed through a sequence of game hops, each a small change to the game justified by one reduction or one statistical argument. What is new in our setting is that the oracles of our games run the compiled libsignal-cli executable.

The proof connects three layers:

1. A security game for PQXDH composed with the Triple Ratchet. The adversary runs many handshakes, turns some of them into ratchet sessions, and attacks the confidentiality and authenticity of ratchet messages. It may corrupt long-term keys and ratchet state, and interleave all of these queries arbitrarily.

2. A byte-level model of libsignal in Lean. The model follows the Rust source closely, down to encodings, key-derivation labels, key schedules and the SPQR state machine.

3. The AArch64 machine code of libsignal-cli (§4). Every ratchet step in the game is one run of this executable in the directory of the party concerned, from its entry point to its final exit_group system call.

We prove that the machine code computes exactly what the model computes, and that the game run on the model is secure. A coupling argument then shows that the game run on the machine code is secure as well (Figure 7).

5.2.1 The Security Game

Our game combines two games from the literature. The handshake oracles are those of the PQXDH key-indistinguishability game of Fiedler and Günther [52]. They let the adversary register honest parties and parties of its own, generate prekeys, initiate and accept sessions, corrupt identity keys and reveal session keys. The ratchet oracles are those of the secure-messaging game of Alwen, Coretti and Dodis [7] (ACD19). They let the adversary send and deliver messages, pose a challenge (encrypt one of two messages of its choice), inject forged messages and corrupt either party’s ratchet state.

A single oracle connects the two halves. The adversary may promote a session that it initiated through the game into a ratchet session. The oracle first checks that the handshake used keys that an honest party published, and that no earlier session used the same ephemeral key. It then starts the Triple Ratchet, including SPQR, for both parties with the real session key of the handshake. Finally, it marks the responder’s signed prekey as revealed in the handshake game: the responder’s first ratchet key is that prekey, so the ratchet needs its secret. The ratchet proof therefore does not rely on that secret staying hidden.

The adversary wins if it guesses which of its two challenge messages was encrypted, or if it gets a forged message accepted. As in ACD19, the game rules out trivial wins, such as decrypting a challenge with state the adversary has just stolen. The game is written once, for any implementation of the handshake and ratchet steps. We write $\mathsf{Adv}^{\mathrm{comp}}(A)$ for the advantage of adversary $A$ in the game run on our Lean model, and $\mathsf{Adv}^{\mathrm{bin}}(A)$ for its advantage in the game run on the executable. Our bounds are concrete: they are stated in terms of budgets that limit the numbers of parties, prekeys, sessions and attacker’s queries (Theorem 2). §C.1 defines the game precisely.

5.2.2 Reductions as Programs

Our theorems assert that efficient reductions exist, so we must make precise what counts as a reduction. One could express reductions as general-purpose Lean functions. However, this choice makes statements of the form “there exists a reduction” vacuous: a Lean function can be noncomputable, for instance by picking the secret key by choice, or arbitrarily expensive.

We therefore write reductions as programs in a small, deeply embedded reduction language with a cost semantics. A reduction runs the adversary exactly once, as a black box and without rewinding, and answers each of its oracle queries by running a handler. If the assumption game has a challenge phase, the reduction may pause the adversary at one query, obtain the challenge, and then resume the same run.

A handler computes on ordinary data, samples coins and queries the oracles of the assumption game. It can operate on keys and group elements only through declared primitive operations, and it loops only up to bounds written in the program. The cost of a reduction is computed from its program text alone.

A reduction is cost-bounded if its cost, its number of oracle queries and the sizes of the values it computes are bounded by explicit polynomials in the game’s budgets, independent of the adversary, and if its program fits a fixed size budget. This rules out a “reduction” that breaks the assumption on its own, for example by exhaustive search or by hard-coding a large table such as a table of discrete logarithms. §C.2 gives the cost semantics.

5.2.3 Main Theorem

We consider two versions of the PQXDH handshake, both with Kyber1024 as the KEM. The first, $H_{\mathrm{lib}}$, is libsignal’s handshake. Like libsignal, it uses a single Curve25519 scalar per party for both X25519 DH and XEdDSA signatures [79], and it derives the session key with HKDF [68], the standard hash-based key-derivation function. The second, $H_{\mathrm{ro}}$, is the same handshake with that HKDF replaced by a random oracle [21]: an ideal, truly random function that every party, including the adversary, can query. (Prior analyses [52, 28] also model this HKDF as a random oracle.) Our game runs $H_{\mathrm{lib}}$.

Our main theorem states that the game run on the executable is secure. Concretely, it gives a bound on $\mathsf{Adv}^{\mathrm{bin}}(A)$, the advantage of any adversary $A$ that respects the budgets. The bound is a sum of two kinds of terms. The first kind is the advantage of a reduction, built from $A$, against one of our cryptographic assumptions. The second kind is a statistical term, such as the probability of a collision or of a decryption failure. One term, $\varepsilon_{\mathrm{mlkem}}(A)$, depends on the adversary itself (see below). The reductions are fixed by the theorem and are cost-bounded, so if every assumption holds, every term is small and no efficient adversary breaks the executable. Clause 1 states this bound for libsignal’s handshake as is. Clause 2 tightens the handshake term when the handshake’s HKDF is modeled as a random oracle.

Theorem 2 (Binary security, simplified). Lean: libsignal_cli_pq_secure_elf_binary_placed Let $N_{\mathrm{id}}$ be the number of honest parties, $N_{\mathrm{spk}}$ and $N_{\mathrm{opk}}$ the numbers of signed and one-time prekeys, $N_{\mathrm{send}}$ the number of initiated sessions (of which $N_{\mathrm{send,opk}}$ use a one-time prekey), $q_{\mathrm{on}}$ the number of handshake queries other than random-oracle queries, $q_{\mathrm{start}}$ the number of promoted sessions, and $q_k$ the number of ratchet queries in the $k$-th session.

1. Security. There are cost-bounded reductions such that, for every adversary $A$ that respects these budgets, and under functional premises on the primitives (§C.7 and §C.8),

   $$\mathsf{Adv}^{\mathrm{bin}}(A) \;\le\; 2\,\varepsilon_{\mathsf{KI}} \;+\; \sum_{k<q_{\mathrm{start}}}\mathsf{Sess}_k \;+\; 2\,N_{\mathrm{send}}N_{\mathrm{spk}}\,\delta_{\mathrm{kem}} \;+\; 2\,\varepsilon_{\mathrm{mlkem}}(A),$$

   where $\delta_{\mathrm{kem}}$ is the probability that Kyber1024 decapsulation fails, $\varepsilon_{\mathsf{KI}}$ is the advantage of a reduction against the key indistinguishability of the handshake, $\mathsf{Sess}_k$ bounds the advantage of the adversary in the $k$-th ratchet session, and $\varepsilon_{\mathrm{mlkem}}(A)$ is the probability that an ML-KEM-768 decryption failure occurs in the game.

2. If HKDF is modeled as a random oracle in the handshake, then the bound holds with $\varepsilon_{\mathsf{KI}}$ replaced by $\beta_{\mathsf{KI}}^{\delta}+\varepsilon_{\mathrm{ro}}$ (defined below).

The terms of the bound are as follows.

• $\varepsilon_{\mathsf{KI}}$ is the key-indistinguishability advantage, against $H_{\mathrm{lib}}$, of a reduction run with $A$. Under the random-oracle idealization of clause 2, $\varepsilon_{\mathrm{ro}}$ is the gap between $H_{\mathrm{lib}}$ and $H_{\mathrm{ro}}$, and $\beta_{\mathsf{KI}}^{\delta}=\beta_{\mathsf{KI}}+2\,N_{\mathrm{send}}N_{\mathrm{spk}}\,\delta_{\mathrm{kem}}$ bounds the key indistinguishability of $H_{\mathrm{ro}}$. Here $\beta_{\mathsf{KI}}$ is a sum of the advantages $\varepsilon_{\mathrm{Sig}}$, $\varepsilon_{\mathrm{ShCr}}$ and $\varepsilon_{\mathrm{GapDH}}$ of cost-bounded reductions against unforgeability of XEdDSA, collision resistance of Kyber1024 (SH-CR [28]) and Gap-DH on X25519, plus public-key collision terms. Each advantage is multiplied by the number of parties, prekeys or sessions that the adversary’s online handshake queries can touch, or by products of these numbers, so the term grows with the adversary’s activity rather than with the size of the deployment (Lemma 1 gives $\beta_{\mathsf{KI}}$ in full).

• $\mathsf{Sess}_k$ bounds the advantage of the adversary in the $k$-th ratchet session as if that key were uniform; the term $2\varepsilon_{\mathsf{KI}}$ pays for replacing the real handshake keys by uniform ones. Following ACD19 [7], it sums the advantages of cost-bounded reductions against the continuous key agreement (CKA) of the DH ratchet, the root key derivation as a PRF-PRNG, and the forward-secure encryption of messages, with further terms for SPQR’s use of HKDF. The remaining terms are statistical. The largest is the probability of forging libsignal’s 8-byte MAC tag, at least $2^{-64}$ per attempt, which grows quadratically in both the number of messages and the number of epochs of the session. §C.9 gives $\mathsf{Sess}_k$ in full.

• For $\delta_{\mathrm{kem}}$, the Kyber specification gives the heuristic estimate $\delta_{\mathrm{kem}}\le 2^{-174}$.

• $\varepsilon_{\mathrm{mlkem}}(A)$ is the probability that, in the game run with $A$, the coins of one or two sends, honest or chosen by $A$, give an ML-KEM-768 key pair and encapsulation whose decapsulation fails. Since $A$ chooses the coins of the sends it injects, this term depends on $A$: it is small unless $A$ can find ML-KEM-768 decryption failures. It is not the advantage of a reduction, because a reduction fixed in advance could hard-code a failing pair.

Proof sketch. The proof has four main parts, stated as lemmas in §C.3.

1. PQXDH (Lemma 1) bounds the key indistinguishability of $H_{\mathrm{ro}}$ by $\beta_{\mathsf{KI}}^{\delta}$. Its proof is a sequence of game hops in the style of [52].

2. Single session (Lemma 2) bounds the advantage of an adversary against one ratchet session, started from a uniform key, by $\mathsf{Sess}$.

3. Composition (Lemma 3) reduces the game run on the model to the key indistinguishability of the handshake and to one single-session game per promoted session, by a hybrid argument over the sessions.

4. Refinement (Lemma 4) states that every run of the executable has the model’s outcome, unless the machine runs out of memory. Its proof is compositional, in a separation logic for AArch64. Each compiled function, from musl’s start-up code and its mallocng allocator through the CLI, protobuf, libsignal and SPQR, gets a contract that relates its registers and memory to the corresponding model function. The contracts are proved by symbolic execution. The lemma holds for every placement of the code in memory that matches the executable, so addresses and relocations are checked against its bytes rather than trusted from the linker.

The theorem follows from the four lemmas by coupling the two games. The game on the executable stores directories where the game on the model stores model states, and the coupling maintains that each directory is the encoding of the corresponding state. By Lemma 4, together with a proof that no run in the game exhausts memory (§4.1), this invariant breaks only if a Kyber1024 decapsulation fails in an honest handshake, which gives the $\delta_{\mathrm{kem}}$ term. Otherwise, the adversary wins both games with the same probability. ML-KEM-768 decryption failures in SPQR are charged once for the whole game: the Lean proof carries out the composition in a game that stops at the first such failure and bounds the probability of reaching it by $2\,\varepsilon_{\mathrm{mlkem}}(A)$.

5.2.4 Assumptions and Idealizations

Cryptographic assumptions. All but two of our assumptions are standard. The two exceptions arise because libsignal uses each party’s long-term Curve25519 secret key for two purposes: to compute X25519 Diffie-Hellman shared secrets in the handshake, and to sign the party’s prekeys with XEdDSA. Standard assumptions treat each primitive on its own, with its own key, and say nothing about whether using one key for both could help an attacker. For example, signatures on chosen messages might help it compute DH secrets, or DH results might help it forge signatures. We therefore use joint-security assumptions [46, 95]: XEdDSA signatures remain unforgeable even for an attacker that can also obtain DH results for the same key, and Gap-DH remains hard even for an attacker that can also obtain signatures under it.

Outside the trusted base, we prove in Lean that both joint assumptions reduce to standard Gap-DH when SHA-512 is modeled as a random oracle (§C.10). The main theorem keeps the joint assumptions, because deriving them from Gap-DH would weaken the bound considerably. Finally, ML-KEM-768 decryption failures are not covered by an assumption; the bound charges them directly as $\varepsilon_{\mathrm{mlkem}}(A)$ (§5.2.3).

Random oracle. Clause 2 of the theorem treats the handshake’s HKDF as a random oracle. This is a heuristic: real HKDF is a fixed function, so clause 2 is not a theorem about it. Clause 1 makes no such idealization, and none of the ratchet’s key derivations are idealized in either clause.

Environment. The routines that libsignal-cli calls through contracts (§4) are assumed to behave as their Lean specifications say. The theorem also assumes functional properties of the primitives, such as that decryption inverts encryption, and fixes features of the process environment, such as the clock, the kernel’s random bytes, the stack size and the available memory (§4.1). §C.5 lists these assumptions. Running out of memory is not assumed away: a proof shows that no run in the game exhausts the available memory (§4.1).

5.2.5 Limitations

Our bounds give no guarantee against a quantum adversary. The symbolic proof covers part of this gap (§5.1). The game also restricts the adversary in ways that the literature does not. The most significant restriction is that the adversary cannot inject its own PQXDH initial message to the responder of a session that is later promoted. Further, the theorem does not cover the privacy of the payload, or the authentication of the responder, for first messages of handshakes that are never promoted. As in ACD19, corruption is refused at some points, for instance while an uncompromised message is in transit. Our game also refuses it until the initiator reaches epoch 10, since until then she may still hold the receiving chain for the leaked signed prekey.

The setting is simplified as well. Each promotion starts one session, messages have a fixed length, and there is no multi-device state. Identity keys are trusted on first use. The statistical terms limit the bound to moderate scale: if nearly every message starts a new epoch, they make it vacuous for single sessions of about $25{,}000$ messages, or for $2^{20}$ sessions of $2^{10}$ messages.

We note that tightening bounds like this is a natural task for AI. Because the theorem’s statement is a Lean definition, a tighter bound is a change to the specification, which humans review, followed by a new proof campaign, which agents carry out.

Finally, the results concern our build of libsignal-cli, run as a fresh process on a machine with the memory of §4.1, not Signal’s own applications, and some of the environment assumptions are argued informally. §C.6 lists the remaining restrictions.

5.3 Trusted Computing Base

The trusted computing base (TCB) is the code that must be audited in order to have confidence that the theorems provide the security guarantees that we claim. To believe our theorems, a reader must check their statements and, transitively, every definition they use. For the symbolic proof, this is the DyLean model and its security statements, the event layer, the concretization function $\gamma$, the refinement statement with its collision clause, and the environment’s restrictions (§5.1.6). The computational proof trusts the definitions of the game, the assumption games and the bound, the Lean model of libsignal and SPQR, and the random-oracle step (§5.2.4).

Both proofs trust (a) the AArch64 semantics and the Lean model of how Linux runs a process (§2.2, §4.1), (b) the contracts of the hooked routines (§4), and (c) the functional and algebraic properties assumed of the cryptographic primitives. These are definitions that are transitively included in the theorem statements. The TCB also includes the tooling that extracts symbol names from the compiler’s object files, and the scripts that build the binary in a reproducible way (§C.6).

Everything else is checked by Lean, including the model-level proofs, the refinement, preservation and coupling arguments, the game hops and reductions, the function contracts and the program logic. For this reason, trusting our proofs also requires trusting Lean itself. The Lean community has invested significantly in trustworthiness of the Lean system, including the design of a small, carefully audited kernel, as well as independent kernels and consistency proofs [36, 37, 16]. Notably, however, the Rust compiler is not trusted. An error in any of the untrusted components that compromises the security properties that we formalize, including a bug in the compiler, or a bug in the Rust code, would cause the theorems to become false, so that the proof would fail.

6 Finding Historical Bugs

To check whether our specifications are strong enough to catch real bugs, we reintroduced two bugs that Cheval et al. [40] found in libsignal and that are now fixed. We injected each bug by reverse-applying its upstream fix commit to the libsignal v0.105.4 source and recompiling the binary, which we call $\mathit{Asm}_{\mathrm{bug}}$.

• Weak state [40, §3.2.1], fix cd36118: a prekey message that fails to decrypt on its new session is trial-decrypted with older sessions, and if that succeeds the new session’s unconfirmed state, which holds a copy of the signed prekey secret, is stored.

• Small subgroup [40, §3.2.2], fix 5293caa: the PQXDH responder does not check that the initiator’s X25519 base key is torsion-free and in range, so a replayed handshake with a mangled base key creates a second session with the same shared secret.

For both bugs we have complete Lean proofs that the symbolic security theorem (§5.1.4) does not hold of the bug-injected binary, $\neg\mathrm{Sec}(\mathit{Asm}_{\mathrm{bug}})$. Recall that $\mathrm{Sec}(\mathit{Asm})$ requires that, for every extern interpretation $\mathcal{I}$ meeting the contracts and every well-formed setup $r$, there exist opaque-symbol byte functions $S$ such that every collision-free hardware trace $\tau \in \mathrm{Traces}_{\mathcal{I},W}(r)$ is explained by at least one reachable model trace ($\mathrm{Expl}(\tau) \neq \emptyset$) and satisfies all ten security queries of Table 2 on every such explanation. Each disproof exhibits concrete witness inputs and splits into two parts: a specification part showing that, under a valid extern interpretation $\mathcal{I}$ and well-formed setup $r$, no choice of $S$ either explains the resulting hardware trace $\tau$, which has fresh coins, in the model or excuses it as a collision; and an implementation part showing that $\mathit{Asm}_{\mathrm{bug}}$ produces $\tau$ under the AArch64 semantics (§2.2).

For the small-subgroup bug, Alice initiates a session and sends a prekey message whose X25519 base key the attacker modifies by setting bit 255, giving a distinct encoding with the same Diffie-Hellman outputs; the model’s canonical-key check rejects this message, whereas $\mathit{Asm}_{\mathrm{bug}}$ accepts it and stores a session. For the weak-state bug, Alice establishes a session with Bob (leaving skipped message keys in Bob’s session file) and then initiates a second session; the attacker splices the second session’s PQXDH header onto an inner message from the first session, which $\mathit{Asm}_{\mathrm{bug}}$ accepts via trial decryption against the stored session while no model transition explains the run. Both disproofs need no assumptions beyond Lean’s standard axioms: the Lean kernel parses the SHA-256-pinned ELF binary $\mathit{Asm}_{\mathrm{bug}}$ and steps its AArch64 machine code across the runs of each witness trace.

On the other hand, refuting the computational theorem is much harder. The theorem states that there exist cost-bounded reductions, against hardness assumptions such as Gap Diffie-Hellman, whose success probabilities bound the advantage of every adversary. To refute it, one must exhibit an adversary that exploits the bug for which every cost-bounded reduction rarely succeeds, which amounts to proving the hardness assumptions themselves, an open problem.

7 AlphaProof Code in Practice

We now describe how we used AlphaProof Code in our verification of libsignal. The proof work was done by a team of five over four weeks, working in parallel on symbolic and computational proofs. Each of us ran agents nonstop on our own workstation, directing specification work and launching proof campaigns on different parts of the system.

Scale. The repository contains nearly 7 million lines of Lean, counting comments and blank lines. About 6.5 million of them are proofs: 5.3 million about the binary, which both security proofs share, about 860,000 for the computational proof and about 350,000 for the symbolic proof. Another 140,000 lines prove the reintroduced bugs (§6), and 70,000 verify the allocator. The verified libsignal code is about 560 KB, about 140,000 AArch64 instructions. The specification directories hold about 54,000 lines, but only part of them is trusted: every file is marked as trusted, trusted in part, or checked by Lean. Reading every definition that our headline theorems depend on means reading about 18,000 lines of code in the repository (about 28,000 with documentation), plus about 8,000 lines of the AArch64 semantics and a Lean representation of the compiled machine code (about 95,000 lines), which a tool extracts from the compiler’s object files; Lean checks its code against the executable’s bytes, so only the symbol names it assigns need to be trusted.

Writing specifications. The most important lesson from our experience is that, once proofs become cheap, the hard question is what to prove. The majority of our effort went not into proofs but into specifications. This trend is perhaps apparent in software development more broadly, but it is particularly acute for cryptographic protocols, where an entire literature is devoted to the question of how to formalize security (§8). One possible future is that programmers write formal security specifications, natural-language intent and performance constraints, and AI generates, optimizes and proves the implementation.

Our specifications were developed through an intense back-and-forth between humans and agents powered by Gemini 4 Carbon and Claude Opus 5.5. For each component—for example, the binary contracts of a libsignal entry point, or the computational main theorem—the specification writer drafted a small set of top-level statements, following a model from the literature where one existed. An agent from a different model family then reviewed the draft for faithfulness to the source paper and to libsignal, for strength (would it rule out known or plausible bugs?), and, where it goes beyond the literature, for consistency with the literature’s conventions. We gave many rounds of targeted feedback before approving a specification and pinning it as the target for proofs. Left to themselves, agents produced specifications that were hard to audit; we sometimes directed rewrites for legibility, which paid off when new team members joined late to review them.

Writing specifications against real code also turned out to be a stress test for the literature. For both formalizations we record every place where the Lean statements depart from their reference papers or from libsignal, together with its effect on the result; the computational catalog has over 200 entries and the symbolic one about 35. Most are routine: the same idea stated differently in Lean, a place where libsignal differs from the scheme analyzed on paper, or a restriction the papers needed for their tools to terminate, which our symbolic model lifts. Some, however, are errors in the published analyses that we had to repair before the proofs could go through. Fifteen are gaps or bugs in the computational analysis of the Double Ratchet [7], such as missing hypotheses and security game conditions that allow trivial wins. On the symbolic side, the printed ProVerif queries of Cheval, Jacomme and Richards [40] look up skipped message keys at the wrong ratchet index, which makes receiver-side forward secrecy false as printed, leave a variable unbound, and bracket post-compromise security so that exposing a party’s own DH key, together with any root-key compromise, excuses a message regardless of when the heal happened. In the PQXDH analysis of Bhargavan et al. [28], reading “some $\mathsf{SPK}_B$ was compromised” literally makes the session-independence corollary unprovable; we bind it to the session’s own signed prekey, as their ProVerif query does.

Generating proofs. The proofs were produced entirely by agent teams powered by Gemini 4 Carbon (§2.3), and none of the authors wrote any proof code. Keeping dozens of agents productive for days at a time is an engineering problem in its own right, and much of our early effort went into the skills that define the agent team. We developed them iteratively by watching campaigns run. A separate agent, above the team orchestrator, serves only as the interface between us and the team: it monitors the team, and we used its logs together with it to diagnose bottlenecks and propose fixes to its processes. Early on, monitoring the team took a lot of human time; this dropped as the skills matured. In the near future, we expect teams like this one to improve themselves.

We summarize a few improvements that emerged through human-AI iterative co-evolution in this way. Agents share notices through a common bulletin file rather than repeating messages. Team leads try to refute their goals before assigning work, fix shared parameters such as stack bounds across callees, and point workers to existing lemmas. Support agents batch expensive Lean builds to fit in memory, watch for stalled agents and exhausted model quotas, and refactor slow modules. The orchestrator reshapes the team as the campaign evolves. Every new invariant an agent introduces must come with a witness that it holds on some reachable state, so that agents cannot make progress by proving vacuous lemmas.

While no human wrote proof code, compute latency was an issue. A clean build of our proofs could take several hours, and early in the project, small source changes or a recompiled binary required large proof repairs. Better program-semantics infrastructure later reduced this. We see substantial room for optimization of proofs generated by and proof techniques deployed by AI.

Preventing specification weakening. Agents under pressure to finish a goal will sometimes weaken it [107, 78], for example by adding a hypothesis or narrowing a precondition, and this can happen indirectly through a definition that the statement depends on: in one swarm of Lean-proving agents, an agent redefined a predicate used in a conjecture’s hypothesis as False, and the trick spread to the rest of the swarm [78]. We therefore never rely on an agent’s own report that a goal is done. The gatekeeper (§2.4) sees only file paths and theorem names, and none of the provers’ dialogue or explanations; Lean replays every proof in a fresh environment, and sorry and native_decide are rejected.

At the same time, freezing the first draft of a specification is too rigid. Even experienced specification writers rarely get every detail right on the first try, and first drafts are often overly conservative in benign ways that make them false of the real code. Our solution is the amendment process of §2.3. An amendment is allowed only if the proof cannot instead be completed with a stronger invariant or a different decomposition, and only if it keeps the non-vacuity witnesses and honest runs covered. A neutral amendment must bring the specification closer to the code. A proposal that would weaken security to match the code is never accepted as an amendment; it is raised to a human as a potential bug. Accepted amendments are small and logged with their justification on an audited branch. Amendments that change trusted assumptions are approved during the campaign, by one of us or under a policy we set (§2.3), and all amendments are reviewed by us at the end of each campaign. One example is extending the composed symbolic query’s handshake-compromise exception from the initial root key to the initial chain key derived alongside it.

The human role. To summarize, we decided the scope and order of the work, chose the reference models, and guided and approved the trusted statements. We also designed the structure of the specifications and guided the overall proof strategy: for example, writing reductions in a small reduction language with a cost semantics (§5.2.2), and, for the symbolic proof, an event layer and concretization homomorphism that maps binary executions to protocol events, together with a refinement to a DyLean model up to collisions that preserves the security properties (§5.1.4). During proof campaigns, we reviewed escalated specification issues and potential bugs, adjudicated amendments that change trusted assumptions, and monitored progress through status logs. We also designed the skills that define the agent team, and refined them as we observed the agents’ behavior. We did not write proofs. Every statement we present as a theorem is checked by Lean, and every assumption we rely on is listed among the trusted definitions (§5.3).

8 Related Work

Analyses of the Signal protocol design. Kobeissi, Bhargavan and Blanchet [67] analyzed a variant of Signal with ProVerif and CryptoVerif. Bhargavan et al. [28] verified PQXDH with ProVerif and CryptoVerif, finding issues in an early version of its specification. Cheval, Jacomme and Richards [40] gave an automated analysis of the Double Ratchet composed with PQXDH, found the two libsignal bugs we re-inject in §6, and proved forward secrecy and post-compromise security. Our symbolic theorems restate theirs and those of Bhargavan et al. with adaptation to connect to our libsignal-cli binary.

On the computational side, Cohn-Gordon et al. [42, 43] gave the first game-based analysis of Signal’s X3DH handshake and Double Ratchet as a multi-stage key exchange. Alwen, Coretti and Dodis [7] defined secure messaging with immediate decryption and proved the Double Ratchet secure in a modular way. Our ratchet game follows their definitions.

Fiedler and Günther [52] analyzed PQXDH in a key-indistinguishability game, which our handshake oracles follow. Both Fiedler and Günther [52] and Bhargavan et al. [28] give each party separate Diffie-Hellman and signing identity keys; Lemma 1 bounds the one-key handshake of libsignal under joint X25519 Gap-DH and XEdDSA unforgeability assumptions [46, 95, 35], while standalone Lean proofs for the two-key key-indistinguishability and first-message authentication models remain in the artifact outside the trusted base.

Verified protocol implementations. Several projects verify implementations rather than designs. miTLS and Project Everest [27] implemented TLS in F$\#$ and proved computational security of the implementation, Noise$^\star$ [59] generates verified implementations of Noise protocols, and LibSignal$^\star$ [83] is a verified implementation of the Signal protocol written in F$^\star$ and compiled to WebAssembly. These are new implementations written for verification; LibSignal$^\star$, in particular, is separate from the production libsignal.

Deployed code has been verified for narrower properties: the s2n TLS library is continuously verified with SAW [41] for functional correctness of its HMAC, DRBG and handshake state machine, and SPQR’s production Rust crate is proved panic-free with hax [25, 90], alongside ProVerif models of its design [89]. Neither proves protocol-level security of the code. One line of work extracts a model from implementation code and verifies the model: fs2pv [26] translates F# code into ProVerif models, Aizatulin et al. [2] extract ProVerif models from C code by symbolic execution, ASPIER [38] abstracts C code into a model that it checks for a bounded number of sessions, and Kobeissi et al. [67] verified a JavaScript implementation of a Signal variant by translating it to ProVerif and CryptoVerif models.

Notably, another line of work annotates the source code itself with specifications and proves them with a type checker or program verifier. Arquint et al. [15] verify annotated Go and Java implementations against a Tamarin model, with a soundness argument that maps model terms to bytes; we follow their concretization in our symbolic refinement. Their main case study gives an end-to-end symbolically verified implementation of the WireGuard key exchange, derived from the official Go implementation of this widely deployed VPN and interoperable with it. To make verification tractable, they modified that code: they removed DDoS protection, metrics and load balancing, and adapted it around stubs for cryptographic and network operations. We verify the libsignal code unmodified. Dupressoir et al. [50] prove protocol properties of annotated C code with a general-purpose verifier.

All of these work either on the source level, on code written or modified for verification, on code in a verification-friendly language, or with a model extracted from source, so the guarantee for the running program relies on a trusted compiler, extraction step or language semantics. We verify the unmodified production library as it is compiled by the stock Rust compiler in a CLI harness (with hooked cryptographic primitives), and state our theorems over machine code. This removes the compiler and the Rust semantics from the trusted base, at the price of reasoning about optimized AArch64.

Mechanized symbolic model cryptography. Symbolic analyses make idealized assumptions about the underlying cryptographic primitives and model the attacker as a Dolev–Yao network adversary that manipulates messages as terms [49]. This focuses the analysis on the protocol design rather than the cryptographic algorithms employed by the protocol. In ProVerif [30, 32], protocols are specified in an applied pi-calculus (process calculus), and proofs are done by translation into Horn clauses, and attacker knowledge is represented as a predicate over these clauses. It permits reasoning about an unbounded number of sessions, but false positives are possible. Tamarin [76, 86] models state as multisets, protocols as multiset rewrite rules, and attacker knowledge as one kind of fact over multisets. Properties are stated in first-order logic over traces. Proofs are solved by constraint solving either automatically or auto-actively. DY$^\star$ [24] proves trace invariants of executable protocol code in F$^\star$, and two recent Lean frameworks build on its approach: DyLean [99], which adds user-defined equational theories and threat models, and LeanDY [63], which combines type-based and trace-based reasoning. Our symbolic specifications and proofs use DyLean, so the protocol model, its security proofs and the AArch64 semantics live in one logic, and Lean’s kernel checks the refinement between them.

Mechanized computational cryptography. Game-based proofs [88, 22] have been mechanized in CertiCrypt [18], EasyCrypt [17], FCF [81], CryptHOL [19] and SSProve [1], among others, and CryptoVerif [31] automates such proofs. Our development builds on VCVio [97], a library for oracle computations in Lean. These frameworks handle the efficiency of reductions in different ways. Some leave it informal, and others restrict reductions syntactically. We write reductions in a small costed language and prove explicit cost bounds (§5.2.2).

Verified cryptographic code. Verified implementations of cryptographic primitives (as opposed to protocols) are complementary to our work, since they specify and verify functional correctness properties (and sometimes constant-time execution) of the primitives that we use in our verification of a cryptographic protocol. Many prior works have verified these primitives, at the C or assembly level, including HACL$^\star$ [108], Fiat Cryptography [51], Vale [34], Jasmin [4], the formally verified ML-KEM in libcrux [44], and the s2n-bignum and AWS-LC proofs in HOL Light [8]. Computational security proofs of cryptographic primitives have been carried down to assembly through verified compilers [5, 6, 3]. To our knowledge, ours are the first proofs of protocol-level security properties for the unmodified code of a widely deployed implementation of a cryptographic protocol.

Verifying code at the binary level. Our AArch64 semantics belongs to a line of work on formal ISA models, including Sail [14], which we test against, Islaris [85], which verifies machine code against such models, and LNSym [55], an Armv8 symbolic simulator in Lean 4. CompCert [73] and the translation validation of seL4 [87] address the gap between source and machine code by verifying the compiler or each compilation. Neither is available for Rust, and source-level Rust verifiers such as hax [25], Aeneas [58] and Verus [71] trust rustc, LLVM and a model of Rust’s semantics, so we verify the compiler’s output directly. Ironclad Apps [57] proved end-to-end security properties of applications at the assembly level, but for applications written in Dafny for verification.

AI for formal verification. Language models have been extensively used to generate formal proofs over the last few years, in both mathematics [82, 103, 62, 96] and software verification. Some efforts in the latter category generate proof annotations in verification-aware languages like Dafny, Verus and F$^\star$ [100, 92, 102, 39]. Others focus on automatically discharging proof obligations for interactive provers [94, 106, 53].

AI capabilities in this area are growing rapidly. In 2025, an agent completed a formalization of the strong prime number theorem in about 25,000 lines of Lean [75]. In September 2026, a multi-agent AI system formalized a proof of Fermat’s Last Theorem in about 13 million lines [9]. In software verification, AI systems have been primarily evaluated on the verification of small individual programs [93, 104], though there is early work on repository-level verification [101].

A number of recent efforts, carried out concurrently with this effort, have highlighted the ability of AI to scale up verification to cover compiled machine code. This includes MachCSL, which verifies the xv6 OS kernel against RISC-V privileged hardware semantics [65], verification of open-source fuzz targets compiled to RISC-V [11], and Zellic’s work on verifying glibc’s startup on x86 [105]. These efforts largely target generic properties, such as crash freedom, or functional correctness. By contrast, our work shows that verifying security of a complex deployed system requires sophisticated specifications, which are substantial engineering projects in their own right. This is why AlphaProof Code supports AI-assisted specification discovery as well as autonomous proof.

9 Discussion

We have introduced AlphaProof Code, a framework in which humans and AI agents collaborate on the formal specification and verification of software, and used it to prove the security of libsignal, the Signal protocol’s reference implementation, at the machine-code level. Our security proofs cover both the symbolic and the computational models. While there is a long line of prior work on formal verification of cryptographic protocols [32, 76, 17, 43, 28, 40, 27, 67], ours are the first proofs of protocol-level security properties for the unmodified code of a widely deployed implementation of a cryptographic protocol.

Our results can be extended in at least three directions. First, the theorems can be strengthened. Our computational theorem is classical, and our ratchet theorems let the attacker choose SPQR’s keys, so neither proves the post-quantum healing that SPQR is designed to provide. The model choices of §5.2.5 and §5.1.6, such as a single session per handshake and fixed message lengths, can be relaxed. Second, the trusted base can be reduced. The two output functions and a few library routines are trusted contracts; verifying them would move the trust boundary down to the system calls. The low-level cryptographic routines have idealized contracts, which could be connected to verified implementations [108, 44]. Third, the scope can be expanded beyond one-to-one sessions, for example, to Signal’s group messaging, sealed sender and server-side protocols.

More generally, our work is one of several recent efforts [11, 65] that point to a shift in the level of abstraction at which code is verified. The attraction of machine-code-level verification is that one needs to trust less—there is no need to model the semantics of high-level languages like Rust and C++ or assume that the compiler is correct. However, proofs at this level are long; when humans wrote almost all formal proofs, they were impractical beyond restricted domains. AI changes this equation by drastically reducing the labor cost of formal proof. That said, verifying at the source level remains a worthwhile way to reduce the compute cost of proof. For example, a substantial fraction of our proofs concerns registers, stack frames and memory layout, which source-level abstractions would hide. Extending our methods to higher-level languages would lower this cost, at the price of trusting the compiler and the language semantics, or of verifying them as well [73, 87].

One lesson is that while proofs are now much cheaper, specifications remain hard. The specification of a nontrivial software artifact is itself a nontrivial software artifact. Developing the software engineering discipline around formal specification is likely to become a fruitful area of research—conceptual frameworks, interfaces, and workflows through which humans and agents develop and validate a formal definition of what correctness and security mean. The process of §7, in which agents draft, review and test specifications under human direction, is a glimpse of how humans and AI might share this work. Like many of the most important problems in software engineering, this is a socio-technical challenge. Specifications of widely deployed systems need to be agreed upon by the communities that maintain, analyze and rely on them. Complex specifications, such as ours, will take many rounds of open review and refinement to settle. We are open-sourcing all Lean specifications and proofs, to facilitate such a process.

In the longer run, we expect AI-driven specification and verification to be tightly coupled with AI-driven coding. Today, verification happens after the code is written, if at all. Once every piece of code comes with a formal specification, and AI proofs are cheap, every change to the code can be verified before it is merged. AlphaProof Code extends naturally to this setting. It treats the specification as a living artifact, revised through reviewed amendments when proofs reveal that it is wrong (§2.3); code changes can be handled the same way, with groups of prover agents repairing the proofs that are affected when the code and (in many cases) the specification change. We are keen to use this workflow to verify new releases of libsignal before they ship, and also more broadly, as well. The coupling of code generation, specification and verification through AI could at last make machine-checked proofs of correctness and security routine for critical systems.

Acknowledgments

We thank Eric Wieser for help with open-sourcing our code, Owen Jones for program management support, and Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko and George Tsoukalas for helpful discussions. We thank Signal’s Rolfe Schmidt, Michael Rosenberg, and Ehren Kret for their feedback on our specifications. We also thank Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis, and Sundar Pichai for their support of the project.

References

A The Signal Protocol in Detail

This appendix gives the details of PQXDH and the Triple Ratchet that §3 omits (Figure 8).

PQXDH. Each party has a long-term X25519 identity key $\mathit{IK}$. Bob uploads to the server a prekey bundle: a signed prekey $\mathit{SPK}_B$ and a Kyber1024 prekey $\mathit{PQPK}_B$ (single-use, or a reusable last-resort key), both signed with $\mathit{IK}_B$ (XEdDSA), and optionally single-use one-time prekeys $\mathit{OPK}_B$. Alice fetches the bundle, verifies the signatures, generates an ephemeral key $\mathit{EK}_A$ and computes $\mathit{DH}_1=\mathsf{DH}(\mathit{IK}_A,\mathit{SPK}_B)$, $\mathit{DH}_2=\mathsf{DH}(\mathit{EK}_A,\mathit{IK}_B)$, $\mathit{DH}_3=\mathsf{DH}(\mathit{EK}_A,\mathit{SPK}_B)$ and, if a one-time prekey was used, $\mathit{DH}_4=\mathsf{DH}(\mathit{EK}_A,\mathit{OPK}_B)$. She encapsulates a secret $\mathit{ss}$ to $\mathit{PQPK}_B$, obtaining a ciphertext $\mathit{ct}$, and derives the session secret $\mathit{SK}$ with HKDF from the DH values and $\mathit{ss}$. The DH values implicitly authenticate the parties, since only the holders of the identity keys can compute them, and $\mathit{ss}$ protects $\mathit{SK}$ against an adversary who records the handshake and later breaks Diffie-Hellman. Her first message, a PreKeySignalMessage, carries $\mathit{IK}_A$, $\mathit{EK}_A$, $\mathit{ct}$ and the prekey identifiers together with her first encrypted message. Bob recomputes $\mathit{SK}$ and deletes the one-time prekey.

The Triple Ratchet. $\mathit{SK}$ is split into a root key, a chain key and a seed for SPQR. In the Double Ratchet [80], the symmetric ratchet derives each message key and the next chain key from the current chain key with HMAC-SHA256, so old keys can be deleted (forward secrecy). Each message carries the sender’s ratchet public key, and a party that sees a new one mixes a fresh DH output into the root key, so an adversary who has compromised a party’s state loses access after the next round trip, provided it does not interfere with that round trip (post-compromise security). This healing holds only against classical adversaries, so the Sparse Post-Quantum Ratchet (SPQR) [89] runs an ML-KEM-768 exchange alongside, with keys and ciphertexts split into chunks carried in ordinary messages; each completed exchange yields an epoch key from which SPQR derives a key per message. The key that protects a message is derived from both the Double Ratchet’s and SPQR’s message keys. The message is encrypted with AES-256-CBC and authenticated with HMAC-SHA256 truncated to 8 bytes, over both identity keys and the protobuf-encoded SignalMessage, which carries the sender’s ratchet key, counters for out-of-order delivery, the SPQR chunk and the ciphertext. The receiver keeps a bounded number of keys of skipped messages.

B Symbolic Proofs

This appendix completes §5.1: the composed model as a transition system (§B.1), the hardware events (§B.2), the concretization function (§B.3), explanations (§B.4), the collision clause (§B.5), the security statement and the scope of the binary theorem (§B.6, §B.7), and the preservation proof (§B.8).

B.1 The Composed Model

Each of the four libsignal entry points corresponds to one atomic transition in DyLean’s Traceful monad (so the DH and SPQR ratchets execute atomically inside messageDecrypt, never exposing a half-ratcheted state). Transitions read from and append to a single global append-only trace (ExecTrace), recording fresh randomness (genRand), network transmissions (sendMessage), immutable session-state snapshots referenced by trace handles (storeLocalState), and protocol events (logEvent). Compromises, exposures and breaks are protocol events (such as CompromisedIK, ExposedRK and BrokenDH); a compromise or exposure then sends the leaked secret on the network. Table 3 summarizes all 23 transitions of the composed state machine (ReachabilityConfig), which store long-term and prekey secrets (PQXDHState) as well as session snapshots (TRState) on the trace; any transition may fire at any time on attacker-chosen arguments whose guards hold.

B.2 Hardware Events Lean: RunEvent Lean: EnvEvent

A hardware trace is a list of events (CliEvents). A run event holds the party, the command, the run’s input, its coins, and its exit code with its standard output. The attacker may invert a key only after the matching break, and only a key that an honest party generated: a key of the setup, or one that a successful run drew from its coins. Table 4 lists every event.

B.3 Concretization Lean: gamma

$\gamma$ (§5.1.4) is defined by recursion on terms: each function symbol $f$ comes with a function on byte strings, and $\gamma(f(t_1,\ldots,t_k))$ applies it to $\gamma(t_1),\ldots,\gamma(t_k)$.

Literals stand for their own bytes, concat appends, trunc8 keeps the first 8 bytes, and the wire-message symbols give libsignal’s protobuf encoding. The cryptographic symbols use an interpretation $\mathcal{I}$, which gives each symbol’s result on its argument bytes. dhPk and dh are X25519, symEnc is AES-256-CBC, Encap is Kyber1024 encapsulation, and kdfExtract is HMAC-SHA256, built in Lean from the SHA-256 compression function. Among the laws assumed of $\mathcal{I}$ is Diffie-Hellman commutativity: dh sorts its two secrets, so both parties compute the same shared-secret term, and commutativity gives them the same bytes. The remaining laws state that X25519 public keys are canonical and never low-order, that agreement reads only the u-coordinate, ignores torsion points and is zero exactly on low-order points, that the binary’s torsion check rejects a public key shifted by a torsion point (without this law the theorem is false, since the MAC does not cover the base key), that AES-CBC decryption inverts encryption and has no junk (a ciphertext that decrypts is the encryption of its plaintext), and that X25519 outputs and libcrux HMAC tags are 32 bytes long. These laws are trusted; we prove only that they are jointly satisfiable.

Two more parameters complete $\gamma$. Some symbols are opaque: the SPQR operations, Kyber1024 public keys, decapsulation of a ciphertext that is not an honest encapsulation, and XEdDSA. Their bytes come from fixed byte functions $S$, which must agree with the setup: they give the setup’s signatures and Kyber public key their provisioned bytes, and decapsulation under Bob’s Kyber prekey agrees with $\mathcal{I}$. Nothing else is assumed about them. A per-trace ghost $g$ gives the bytes of each fresh value: those of the piece of a run’s coins, or of the plaintext of a send run, that it is matched with, or, for the setup’s keys, the setup’s bytes. It also gives the bytes of each wire message’s addresses field, which has no model term. The ghost is the only part of $\gamma$ that depends on the execution.

B.4 Explanations Lean: MatchesEvents Lean: Explains

Each transition along a model trace (§5.1.1) corresponds to at most one event from Table 4, carrying symbolic terms rather than bytes: for example, encrypting a message corresponds to a send run whose input is a fresh plaintext term, whose coins are fresh coins, and whose output is a wire-message term; compromising a secret corresponds to a leak; and a rejected run leaves the model state unchanged. A model trace matches a hardware trace $\tau$ if these events line up with $\tau$’s events one to one, in order, and each byte field of a hardware event equals $\gamma$ applied to the corresponding model term(s) under libsignal’s wire and key encodings.

A model trace explains $\tau$ if it is reachable in the model, matches $\tau$, and agrees with the execution on details that the hardware events do not record. Because $\tau$ records only what goes into and out of each run, it omits how stored session records overwrite prior state from run to run, and how incoming bytes were decoded and routed internally. Pinning explanations to these unlogged details prevents the model trace from reusing replaced session state or logging handshakes the binary did not perform when we evaluate the security queries on it, and—in the collision clause below—rules out degenerate explanations of a trace prefix.

B.5 The Collision Clause

The collision clause of the refinement definition (§5.1.4) excuses only runs that no explanation can account for without a collision between two different terms, at least one built by a symbol assumed injective. No opaque symbol is assumed injective. Two further clauses concern the truncated MAC: a received message is also excused if its 8-byte MAC equals one that the receiver computes from a ratchet seed the attacker does not know (a guessed MAC), or one computed under a different seed. Three features constrain the collision case. First, $S$ is chosen before the hardware trace, and opaque bytes are never assumed injective, so $S$ cannot be tuned to create collisions. Second, for a received message the collision must occur under every explanation of the prefix that has not already read a colliding message (except in the Kyber case below), so the proof cannot pick an explanation that happens to collide. Third, a received message counts as a collision only if every term the attacker knows that the model would accept for it itself involves a collision: once the attacker has leaked or inverted a key, a message it forges with that key must be explained, not excused.

One further clause concerns Kyber: a decapsulation that disagrees with encapsulation is excused, since no Kyber correctness law is assumed on $\mathcal{I}$; hardware traces in this case get no guarantee. The clause reads only the interpretation $\mathcal{I}$, the setup and the received ciphertext, never $S$, the ghost or the run, so it holds only if decapsulation under Bob’s provisioned key disagrees with encapsulation on that ciphertext: the hooked Kyber implementation is incorrect, the provisioned key is malformed (key generation is not verified, and well-formedness checks only the public key embedded in the secret key), or the ciphertext is one of the decryption failures that Kyber1024 has with negligible probability. (Kyber’s implicit rejection of a malformed ciphertext is modeled directly in the symbolic KEM by a secret-keyed rejection symbol, so it is explained rather than excused.)

B.6 The Security Statement

For initiator secrecy, for instance, the query in $Q(\mathit{tr}, K)$ says that if Alice completed a handshake in $\mathit{tr}$ and one of its keys is in $K$, then one of that row’s excuses of Table 5 holds on $\mathit{tr}$. The ten properties differ only in $Q$, where each is one conjunct: stated alone, each has exactly the shape of Theorem 1 with its own query in place of $Q$, and Theorem 1 implies all ten of these statements, with one common $S$, because $Q$ is their conjunction. Table 5 states every query using the event shorthands defined next (for the events of Table 3).