Can we prove that Signal's cryptography is secure — not just on paper, but in actual (source and proof) code? Signal Shot aims to find out. We're verifying the Signal protocol and its Rust implementation using the Lean Proof Assistant, in a public moonshot to show that formal verification of major applications is doable today. Think of it as the Liquid Tensor Experiment (LTE) for cryptography — where a complex math theorem was formalized and proved with the help of the mathematics community — except this time, we also have steadily improving AI on our side.

Here's how we'll do it: first, we write down a mathematical model of the protocol and prove its security properties. Then, we take Signal's existing Rust implementation and translate it to Lean using the Aeneas tool. Finally, we verify that the translated code actually satisfies the assumptions of our proven model — bridging the gap from theory to real-world code.

For more details visit our Signal Shot page.

How It Started

The moonshot began as a convergence of three distinct, multi-year research problems spanning protocol security, formal verification and AI assistance. This ambitious convergence was driven by the long-standing goals of three key leaders in the field:

Rolfe Schmidt at Signal has spent years designing post-quantum protocols like PQXDH and SPQR, juggling tools like ProVerif, CryptoVerif, and pen-and-paper proofs. His dream: one tool — not just for machine-checking the full protocol stack, but also for designing new protocols and for continuous verification as the software evolves.

Leo de Moura at Lean FRO built the Lean Proof Assistant, combining the best of SMT solvers and tactics-based reasoning. His dream: a software verification framework built collaboratively by research and engineering communities, practical and powerful enough to tackle real-world code, and seamlessly connected with AI models that can help write specs and proofs.

Max Tegmark founded the Beneficial AI Foundation to build capabilities for AI safety, scaling up software verification through a combination of AI tools, open-source software tools and open standards. He seeks a virtuous cycle: better AI tools driving formal verification adoption, which in turn produces more verified code to train still better AI tools.

With Signal Shot, we hope to build on their collective experience, and to invite the larger community to join us on this journey.

Launch Stages

The Signal protocol is a stack of interlocking components, each of which needs verification:

Cryptographic Infrastructure — the foundational primitives
PQXDH — the post-quantum key exchange
Double Ratchet — encryption for forward and backward secrecy
SPQR/Triple Ratchet — the post-quantum ratchet extension
Functional Correctness — bridging proofs to actual Rust code
Anonymous Credentials — identity without exposure
Session Management — handling real-world connection state
Protocol Composition — proving the pieces work together securely

Just as a rocket is accelerated in stages, we are tackling this stack incrementally. In the early stages, we focus on the core protocol properties, with domain experts checking critical definitions. In parallel, we use the Aeneas tool to translate Signal's Rust implementation to Lean. Meanwhile, the functional correctness team formalizes simpler, well-understood concepts — getting the machinery oiled and ready for the hardest verification challenges ahead.

Scaffolding for Collaboration

An essential collaboration tool for the Liquid Tensor Experiment was Blueprint, a LaTeX-based tool used for outlining proofs, registering stubs, and tracking tasks among collaborators in math theorem proving. VeriLib is a platform developed by the Beneficial AI Foundation, engineered to do the same for software verification. It not only provides a collaboration framework but also automatically extracts and visualizes metadata on every component, or atom, of the code.

Outlines — Collaborators can use Verso-Blueprint (based on Lean rather than LaTeX) for informally outlining the definitions, theorems, and proofs.

Analysis — VeriLib parses and probes both Rust and Lean source code, and provides an integrated view of each Rust atom with its Lean translation and Lean specifications. It also calculates and displays the dependencies between the functions, definitions and theorems.

Tasks — Collaborators can view the formalization, validation and verification statuses (represented as white, blue and green bars) of each atom, as well as the status of the whole project. Soon, we will be able to generate Issues on GitHub with the click of a button. We can see which issues still require help.

Certification — At the end of the day, VeriLib will run the Lean verifier on the entire code base, and generate a certificate as proof that the verification was a success. This certificate will be stored on the Ethereum blockchain.

Engines for Proofs

Our vision extends beyond protocol verification: we are building general proof tools to revolutionize all software verification efforts.

Transpilation — Dramatically increase the fraction of production Rust code that the Aeneas tool can successfully transpile to Lean.
Compilation — Accelerate compilation by the Lean proof checker, aiming for proof automation speed comparable to that offered by SMT-solver-powered Automated Theorem Provers (ATPs).
Frameworks — Foundational improvements to the Std.Do framework for reasoning with monadic programs (e.g., imperative programs) through the generation of verification conditions.
Libraries — Expand CSLib and Mathlib support for complex proofs involving elliptic curves, module lattices, or advanced cryptography, and for enabling symbolic and computational proofs of security protocols.

Intelligence for Formalization

Formal verification has always been bottlenecked by human effort — the painstaking translation from intuition to formalism. AI changes that equation.

We envision a collaboration where humans focus on what they do best: understanding the deep structure of a proof, choosing the right abstractions, spotting the subtle flaws. AI handles the rest — auto-formalizing research papers, expanding proof sketches into detailed verification plans, translating theorems into Lean, and grinding through the tedious proof steps. The result: verification that scales with complexity, not just headcount.

How It Will Fly

A moonshot like this needs more than ambition. Learning from the success of the Liquid Tensor Experiment, we will adhere closely to the following three key guiding principles.

Specs — We will write informal narratives that outline the proof strategy before diving into formalization, and bring in domain experts to validate key definitions and specifications early.
Proofs — Because proofs are living artifacts, we will organize them for robustness — so they survive refactoring as the project evolves.
People — A small core of passionate researchers will dedicate themselves to driving the effort forward, with careful prioritization to keep things on track.

Next Small Steps

Signal Shot is an open, collaborative mission, and we are actively seeking contributors. If you're a cryptographer, protocol designer, Lean developer, Rust engineer, or formal methods researcher — there's a place for you here. Pick a component. Tackle a proof. Improve the tooling. Every contribution moves us closer to a world where critical infrastructure isn't just tested, but proven secure. Visit the Signal Shot page to see open problems, track progress, and find your entry point into the mission.

Signal Shot: One Giant Lean for Protocol Security