Signal Shot: Lean's Moonshot to Verify Signal's Code

The landscape of software verification is about to shift dramatically. A new initiative called Signal Shot has emerged as a public moonshot to verify not just the mathematical foundations of the Signal protocol, but the actual Rust implementation that billions of people rely on for secure communication.

This isn't theoretical mathematics on paper. This is proving that the code running on your phone is mathematically correct. The collaboration brings together Signal (represented by Rolfe Schmidt), the Beneficial AI Foundation (led by Max Tegmark), and the Lean FRO in what could be a watershed moment for both cryptography and formal verification.

The reference point for this ambitious project is the Liquid Tensor Experiment. Nearly four years ago, Johan Commelin's team formalized the main theorem of liquid vector spaces by Clausen and Scholze in Lean. That achievement demonstrated that Lean could scale to handle modern mathematics. Signal Shot asks whether Lean can now scale to verify deployed software that people actually use.

What makes this possible now is the convergence of several critical technologies that simply didn't exist together until recently.

The Technical Foundation

At the heart of Signal Shot is Aeneas, a Rust-to-Lean functional translator developed by Son Ho during his INRIA PhD thesis "Formal Verification of Rust Programs by Functional Translation." This tool, which earned the Gilles Kahn PhD thesis award from the French Academy of Science in 2025, already powers verification work inside Microsoft on SymCrypt. Aeneas transforms libsignal's actual Rust code into something that can be formally proven about, without requiring Signal to maintain a separate codebase solely for verification purposes.

The mathematical infrastructure comes from Mathlib, which holds the cryptographic foundations: elliptic curves, module lattices, and the reductions that cryptographic proofs rely on. Complementing this is CSLib, a new Lean library aiming to be for computer science what Mathlib is for mathematics. The cryptographic primitives and protocol-level definitions that Signal Shot needs will live in CSLib.

Two new tools form the verification backbone: grind and SymM. grind is an SMT-inspired tactic featuring congruence closure, E-matching, linear arithmetic, and theory solvers. SymM is a new monadic framework specifically built for software verification. Started in December 2025 right after the Lean@Google Hackathon, SymM implements maximally shared terms, efficient metavariable management and simplifiers, and several custom tactics required by verification condition generators.

The performance difference is staggering. On software-verification benchmarks, SymM is orders of magnitude faster than the standard MetaM infrastructure. It turns quadratic blowups into linear passes, delivering roughly a 100x speedup on stress tests that were bringing the old machinery to a halt. Aeneas is currently being ported onto SymM, and the first public discussion of these developments will occur at the Lean Paris Hackathon on April 20, titled "Scalable Software Verification in Lean 4" at SViL2026.

The AI Revolution in Formal Verification

The most transformative element is artificial intelligence. Not long ago, this entire endeavor would have been impossible. Today, teams are already doing serious mathematical formalization in Lean and Mathlib with heavy AI assistance.

Math Inc. provides a compelling example: they recently autoformalized Viazovska's Fields-Medal proof on sphere packings in weeks, not years. Other teams are achieving comparable results. The expectation for Signal Shot is that AI models will handle the autoformalization and routine work, while humans focus on choosing abstractions and spotting subtle flaws.

This division of labor is crucial. As Terence Tao observed, reinforcement learning finds every backdoor in your verification pipeline, so there cannot be any. The kernel's soundness becomes AI safety infrastructure. Multiple independent kernel implementations exist at arena.lean-lang.org, ensuring that a proof produced by Signal Shot is a proof any reviewer can check independently, without trusting the people who wrote it.

The Path Forward

Signal Shot is explicitly open. The project needs contributors across multiple domains:

• Mathlib contributors to develop the cryptographic primitives
• CSLib contributors to build protocol specifications
• Lean hackers to help Aeneas scale to libsignal and build the verification pipeline with benchmarks, regression tests, and glue code
• Cryptographers to review definitions before proofs begin

The LTE proved that mathematics scales in Lean. Signal Shot asks whether deployed software can scale in the same way. The first update will come at the Lean Paris Hackathon on April 20, where most of the Signal Shot collaborators will be present.

This moonshot represents more than just verifying one protocol. It's a test case for whether formal verification can move from academic exercises to practical tools that ensure the security of the software billions of people depend on daily. If successful, Signal Shot could establish a new standard for cryptographic software verification, where the actual running code is mathematically proven correct rather than just the abstract protocol it implements.

The stakes are high. The tools are ready. The collaboration is in place. What remains is the work of proving that the code securing our most private communications is as mathematically sound as the theorems that underpin modern cryptography.