Signal Shot¶
A moonshot initiative to formally verify the Signal protocol and the Signal app using the Lean theorem prover. Co-led by the Beneficial AI Foundation, Signal, and the Lean FRO, with 20+ academic and industry collaborators including Cryspen, Stanford, UC Berkeley, Google, and Microsoft.
Launched 20 April 2026 at the Software Verification in Lean workshop in Paris.
| Repo | Beneficial-AI-Foundation/signal-shot (public, MIT) |
| Project page | beneficialaifoundation.org/signal-shot |
| Chat | Zulip — #Signal-Shot |
This is a research program, not a VeriLib platform component
Signal Shot is a verification effort that uses the same tooling ecosystem — Lean, Aeneas, and the probe family. It is not part of the VeriLib web platform. Its repository is the source of truth; this page is an index entry.
Why it matters¶
Three intertwined goals:
- A reference for shipping verified software — tools not just for end-to-end machine-checking of full protocol stacks, but for designing new protocols and for continuous verification as software evolves.
- Catalyze software verification in Lean — improve tooling and performance, bring the Lean verification ecosystem together, and connect AI-assisted formalization to software verification.
- Build capabilities for AI safety — scale verification through AI tools, open-source software, and open standards, in the same virtuous cycle VeriLib is built around: better AI tools drive verification adoption, which produces more verified code to train still better tools. See About VeriLib.
Two tracks¶
The project runs along two parallel, complementary tracks. Most contributors find one a more natural fit; both feed the same end goal.
| Track | What it does | Suits you if |
|---|---|---|
| Functional correctness | Verify that Signal's Rust implementations match their specifications. Rust source is translated into Lean using Aeneas, then the translated code is proved to satisfy its spec. | You enjoy reading code and pinning down what it actually does |
| Protocol security | Formalize the cryptographic protocols Signal uses as mathematical models and prove their security properties — secrecy, authenticity, forward secrecy, post-compromise security | You are drawn to cryptographic reasoning and protocol models |
The Aeneas-based functional-correctness track is the one that overlaps most directly with VeriLib tooling: Aeneas projects are exactly what probe-aeneas extracts, producing the cross-language Rust + Lean graphs whose progress is tracked in Verification progress metrics.
Related repositories in the org¶
Several public repos are part of or adjacent to this work:
| Repo | Role |
|---|---|
| signal-shot | Program hub |
| libsignal-verify, libsignal-verus | Verification of libsignal |
| secure-messaging, cslib-protocols-lean | Protocol-security track |
| aeneas, rust-lean | Rust → Lean translation |
Each documents itself; this hub does not mirror them.
Contributing¶
Start at the signal-shot README and the Zulip channel. For CI patterns used across Lean verification repos in the org, see Verification in CI.