Formally Verifying Signal: What It Actually Means to Prove a Cryptographic Protocol and Its Rust Code

Leo de Moura, the creator of Lean and Z3, announced that the Signal Shot platform is ready, marking a significant milestone in an ambitious project to formally verify both the Signal messaging protocol and its production Rust implementation. This is worth stopping to think about carefully, because the phrase “formally verified” gets thrown around in ways that obscure what is actually hard about this kind of work and why the Signal case in particular is unusually demanding.

What Signal Shot Is Trying to Do

Signal Shot targets two distinct layers of correctness at once. The first is the protocol level: verifying that the Signal protocol’s cryptographic design achieves its stated security goals, things like forward secrecy, break-in recovery, deniability, and resistance to key compromise impersonation. The second is the implementation level: verifying that libsignal, the Rust library that implements the protocol in production, correctly and completely realizes the specification.

Most prior formal verification of messaging protocols stops at the first layer. Tools like ProVerif and the Tamarin prover excel at finding flaws in protocol logic. Researchers have used both extensively on Signal. A 2016 paper by Cohn-Gordon, Cremers, Dowling, Garratt, and Stebila analyzed the Signal protocol in a symbolic model using Tamarin, producing security proofs for the X3DH key agreement and the Double Ratchet algorithm under various threat models. A follow-up in the computational model filled in the remaining gaps. By most accounts, the protocol design is solid.

But a verified protocol is not a verified application. The gap between a mathematical proof about a protocol’s abstract operations and the behavior of actual compiled code running on real hardware is where most real-world vulnerabilities live. Signal Shot is trying to close that gap using Lean 4.

Why Lean 4 Is Interesting Here

Lean 4 is unusual among proof assistants because it is also a practical general-purpose programming language. Most of its predecessors, including Coq and Isabelle/HOL, are purpose-built for formal reasoning and use extraction mechanisms to produce runnable code from proofs. Lean 4 inverts this relationship: you write programs in Lean directly, and the same language is used for the logic. This matters for the Signal Shot approach because it means you can express the specification, the proof, and potentially executable models all within the same framework without translation layers that could introduce their own bugs.

The Lean 4 mathematical library, Mathlib, has grown substantially and now includes a serious body of algebraic and number-theoretic results. Elliptic curve arithmetic over fields like the ones underlying Curve25519 is well within scope. This gives Signal Shot a foundation for reasoning about the cryptographic primitives Signal relies on, rather than treating them as black boxes.

The Signal Protocol’s Structure Makes This Hard

Signal’s security comes from two interlocking mechanisms. X3DH (Extended Triple Diffie-Hellman) establishes an initial shared secret from a combination of long-term identity keys, signed prekeys, and one-time ephemeral keys. The Double Ratchet algorithm then uses that initial secret to derive a continuously evolving chain of message keys, advancing the ratchet on every send and receive.

The Double Ratchet is particularly interesting to verify formally because its security properties are inherently stateful and temporal. Forward secrecy means that compromising the current state should not reveal past messages. Break-in recovery means that even after a full state compromise, security should be restored after enough subsequent messages. Capturing these properties in formal logic requires reasoning about infinite sequences of state transitions, which is exactly the kind of argument that interactive theorem provers are designed for but that automated model checkers struggle with at scale.

The Rust implementation adds another dimension. libsignal is a non-trivial codebase that handles low-level byte manipulation, session state serialization, and platform-specific crypto backends. Rust’s ownership model eliminates many memory-safety concerns, but it does not prevent incorrect logic, missed state transitions, or subtle deviations from the specification.

Bridging Rust and Lean

Verifying Rust code from within Lean is an active research area. The most mature approach is Aeneas, a toolchain developed by Ho, Protzenko, Fromherz, and Bhargavan that translates Rust’s Mid-level Intermediate Representation (MIR) into functional specifications in Lean 4 or F*. Aeneas handles Rust’s ownership and borrowing through a system of “loan” abstractions that make the aliasing constraints explicit in the functional model, so you can then prove properties about the resulting pure functions.

This approach has been used to verify real Rust code. The Crux-MIR project from Galois takes a related path using symbolic execution. Signal Shot’s use of Lean suggests it is likely working in the Aeneas tradition or developing similar infrastructure, with the advantage that the spec and the proof can all live in the same Lean environment.

A simplified sketch of what this looks like in practice: you take a Rust function like the one advancing the sending ratchet, translate it to a Lean function over abstract state, and then prove that this Lean function satisfies a predicate expressing forward secrecy. The challenge is that the translation needs to be trusted or itself verified, and the abstract state needs to faithfully represent what the Rust code actually manipulates.

-- Sketch of what a Double Ratchet step specification might look like in Lean 4
structure RatchetState where
  rootKey    : Key
  sendChain  : ChainKey
  recvChain  : ChainKey
  sendCount  : Nat
  recvCount  : Nat

def advanceSendRatchet (s : RatchetState) : RatchetState × MessageKey :=
  let (newChain, msgKey) := kdfChain s.sendChain
  ({ s with sendChain := newChain, sendCount := s.sendCount + 1 }, msgKey)

-- A property: message keys derived from different ratchet steps are independent
theorem sendKeys_independent (s : RatchetState) (i j : Nat) (h : i ≠ j) :
    (nthSendKey s i) ≠ (nthSendKey s j) := by
  sorry -- the actual proof is where the work lives

The sorry in that sketch is not a cop-out; it is where the mathematical substance of the security argument lives, and completing it requires real cryptographic reasoning, not just type-checking.

Prior Work and What Makes This Different

Formal verification of cryptographic protocols has a long lineage. The EasyCrypt framework has been used to verify constructions in the computational model, where the adversary is a probabilistic polynomial-time algorithm and security is expressed as bounds on distinguishing advantage. F*, developed at Microsoft Research and INRIA, was used to produce a verified implementation of TLS 1.3 in the HACL* and miTLS projects. F* targets a similar goal: write code in the verification-aware language, prove it correct, and extract or compile to C.

Lean 4 brings a different set of trade-offs. Its metaprogramming capabilities are more flexible than F*‘s, and the Mathlib library provides a broader base of mathematical results. The disadvantage is that Lean 4 is a younger ecosystem for this specific application domain, so Signal Shot is partly building infrastructure as it goes.

What distinguishes Signal Shot from most prior work is the explicit scope: both the protocol and the production implementation, in a single coherent framework. The HACL* project produced verified implementations of individual primitives like Curve25519 and ChaCha20-Poly1305, but Signal’s security depends on how those primitives are composed, and composition is where subtle errors appear.

Why This Matters for Signal Specifically

Signal is not academic software. It runs on hundreds of millions of devices and is used by journalists, activists, and people whose physical safety depends on communications security. The libsignal library is the reference implementation that other Signal-compatible clients build on. A verified implementation would not just be an academic result; it would directly improve the security guarantees of a widely deployed system.

The alternative is the current state of affairs: careful code review, extensive testing, and third-party security audits. These are valuable, but they are not proofs. Audits can miss subtle logical errors, and tests can only cover paths the tester thought to exercise. A formal proof, if the trusted computing base is small and well-understood, covers all possible inputs and execution paths.

The announcement that the platform is ready suggests the infrastructure for connecting Lean proofs to the Rust codebase is in place, even if the full security theorems are still being developed. This is the hard part of the engineering: getting the toolchain, the translations, and the proof state infrastructure to the point where the actual mathematical work can proceed efficiently. It is the kind of milestone that does not generate headlines but determines whether a project like this can realistically be completed.

What Comes Next

The natural progression from here is filling in the actual proofs of the security properties. For the protocol layer, this means stating and proving that X3DH achieves authenticated key exchange under the right assumptions, and that the Double Ratchet maintains its invariants across arbitrary sequences of sends, receives, and potential key compromises. For the implementation layer, it means proving that every function in libsignal that handles key material matches its abstract specification.

The cryptographic assumptions underlying Signal, specifically the hardness of the Diffie-Hellman problem over Curve25519 and the security of HKDF and HMAC, will likely be taken as axioms rather than proven from scratch. This is standard practice and does not weaken the result, since the same assumptions underlie every deployed system using these primitives. The value of the proof is in showing that the protocol and implementation are correct given those assumptions, not in re-deriving the assumptions themselves.

If Signal Shot reaches completion, it would join a small group of large-scale verified cryptographic systems. The work deserves attention from anyone who thinks seriously about what it means for software to be secure, not just tested.