Formal verification of cryptographic protocols has a long and productive history. Tools like ProVerif and Tamarin have been used to verify properties of TLS, Signal, and dozens of other protocols. Researchers have proven that the Double Ratchet algorithm achieves forward secrecy, that X3DH provides authentication against active attackers, and that Sealed Sender leaks less metadata than naive approaches. These results are real and they matter.
But all of them work on models, not code.
When you verify a protocol in ProVerif, you write a process calculus description of the protocol. When you verify it in Tamarin, you write multiset rewriting rules. The actual Rust or C code that ships in Signal’s apps is a separate artifact, related to those models by intention but not by proof. The gap between a verified model and a deployed implementation has historically been where the interesting bugs live.
Signal Shot is a project led by Leonardo de Moura, the creator of Lean, to close that gap. The goal is to formally verify both the Signal protocol specification and its Rust implementation in libsignal, with Lean 4 as the verification language. The recent announcement is that the platform for doing this work is now in place, which is itself significant: building the infrastructure to even attempt implementation-level verification of a production cryptographic library is a substantial engineering task.
Why Implementation Verification Is Harder
To understand what Signal Shot is attempting, it helps to know why implementation verification has historically been left to specialized tools rather than general proof assistants.
Verifying a cryptographic implementation means you need three things: a formal specification of what the code should do, a formal model of what the code actually does (its semantics), and a proof that the two agree. For a protocol like Signal, the specification is itself informal; the Signal protocol documentation is well-written but not machine-checkable. Formalizing it is a contribution in its own right.
Modeling Rust semantics is the other hard part. Rust’s type system enforces memory safety through ownership and borrowing, which is a genuine semantic constraint that needs to be captured correctly in any formal model. Projects like RustBelt have built semantic models of the Rust type system in Iris and Coq, and tools like Charon and Aeneas translate Rust programs through an intermediate representation into functional programs in proof assistants, including Lean. Verus takes a different approach: it annotates Rust source with specifications and discharges proof obligations using SMT solvers.
The Lean ecosystem is well-positioned for the specification side. Lean 4’s type theory (the Calculus of Constructions with inductive types) is expressive enough to state essentially any mathematical property, and Mathlib provides a large library of algebraic and number-theoretic results that are directly relevant to elliptic curve cryptography. Proving that Curve25519 scalar multiplication behaves correctly with respect to the group law is exactly the kind of thing Mathlib can support.
What Gets Verified and What That Means
Cryptographic security proofs come in two flavors: symbolic and computational. Symbolic proofs (the kind ProVerif and Tamarin produce) treat cryptographic primitives as perfect black boxes. Encryption is modeled as a function that only the key holder can invert; there is no notion of hardness assumptions or reduction to mathematical problems. This model is highly automated and scales to large protocols, but it does not capture everything. It cannot tell you whether a particular elliptic curve implementation is vulnerable to timing side channels, or whether the HKDF instantiation leaks bits through a subtle correlation.
Computational proofs, by contrast, work in a probabilistic model and reason about adversary advantage as a function of computational resources. EasyCrypt is designed specifically for this kind of proof. Its probabilistic relational Hoare logic lets you state and prove that an adversary’s advantage in breaking some security property is bounded by some expression involving the hardness of the underlying primitives. This is stronger, but correspondingly harder to automate and more expensive to carry out.
For implementation verification you need the computational picture, because the implementation makes concrete choices that affect concrete security. When libsignal calls into its AEAD implementation, the security of that call depends on the actual nonce construction, the actual key schedule, the actual output size. Lean 4 is a general proof assistant; it can support computational security arguments, though the proof infrastructure is less mature than EasyCrypt’s purpose-built support.
The properties Signal Shot will want to establish for the protocol include:
- Correctness: an honest sender and receiver complete the protocol and agree on session keys
- Confidentiality: a passive network adversary learns nothing about message contents
- Forward secrecy: compromise of a party’s long-term key does not reveal past session keys
- Break-in recovery: after a compromise, fresh randomness ratcheted into the state eventually restores security
- Deniability: messages cannot be cryptographically attributed to a specific sender to a third party
For the implementation, there are additional properties that do not appear in symbolic proofs: correct serialization and deserialization of protocol messages, absence of integer overflows in key schedule arithmetic, correct zeroization of sensitive key material after use.
The Rust Verification Problem
The cleanest existing approach to verifying Rust code in a proof assistant is the Charon/Aeneas pipeline. Charon is a compiler plugin that extracts an intermediate representation from Rust’s MIR (the mid-level intermediate representation that encodes ownership and borrowing explicitly). Aeneas then translates this into a pure functional program using a monad to handle mutable references, and the functional program can be reasoned about in Lean, Coq, or F* without needing to encode Rust semantics directly.
The translation is not trivial. Rust code that uses interior mutability, raw pointers, or unsafe blocks does not translate cleanly into a pure functional setting. Cryptographic implementations often use unsafe code for performance-critical paths, particularly when interfacing with platform-specific assembly for operations like field multiplication on Curve25519. Signal Shot will need either to verify that the unsafe portions are safe (which requires a model of the underlying memory), or to treat those portions as trusted axioms and verify the rest.
This is exactly the approach that HACL* took with F*: verify the high-level protocol logic and verify the low-level cryptographic primitives separately, then compose the proofs. HACL*‘s verified implementations of Curve25519 and ChaCha20-Poly1305 are now used in Firefox, and the approach has been validated by deployment. Signal Shot is attempting something similar in Lean, with a Rust codebase rather than a C codebase.
Why This Matters Beyond Signal
The Signal protocol is not just used in Signal. Its design is deployed in WhatsApp, Google Messages, and a variety of other messaging systems. A mechanized, machine-checked proof of the Rust implementation would be a reference artifact that the entire ecosystem could rely on. More importantly, the tooling and proof infrastructure developed for Signal Shot would be reusable for verifying other cryptographic protocols implemented in Rust.
The Lean 4 ecosystem is growing quickly. The combination of a dependently-typed language with fast compilation, a large mathematical library, and active development from a team with deep expertise in both programming languages and theorem proving makes it a credible venue for this kind of work. The Lean FRO (Focused Research Organization) is investing directly in making Lean useful for software verification, not just mathematics.
The announcement that the platform is ready means the scaffolding exists: the Lean libraries for reasoning about the relevant algebraic structures, the tooling to connect Lean proofs to Rust code, and presumably a formalized specification of the Signal protocol in Lean. The actual verification proofs are the next phase. That work will likely take years and will surface interesting gaps between what the Signal specification says and what the implementation does, which is precisely the point.
Formal verification does not eliminate bugs. It pushes bugs into the specification, into the threat model, or into the assumptions about the underlying hardware and operating system. But for a protocol that hundreds of millions of people rely on for genuinely sensitive communication, finding those remaining gaps through machine-checked proof is worth the effort.