Signal Shot
About
Updated 05/18/26Signal Shot is a public moonshot led by the Beneficial AI Foundation, in collaboration with Signal and the Lean community, to formally verify the Signal protocol and the Signal app’s Rust implementation. Launched in April 2026 at the Software Verification in Lean workshop, the project seeks not only to derive a mathematical model of the protocol and prove its security properties, but also to translate Signal’s production Rust code into Lean and prove that it correctly implements the verified model. The initiative is structured in stages that cover the cryptographic infrastructure, post‑quantum key exchange (PQXDH), ratchet protocols such as SPQR, and functional correctness links between proofs and real‑world code. Signal Shot aims to develop reusable verification tooling, establish a blueprint for shipping verified software, and demonstrate that large‑scale formal verification of widely used applications is feasible today with Lean and AI‑assisted proof tools.
Theory of Change
Signal Shot’s theory of change is that demonstrating end‑to‑end formal verification of a widely deployed, security‑critical application will catalyze broader adoption of verified software and AI‑assisted formal methods. By building open‑source tooling, reference workflows and community capacity around Lean‑based verification of the Signal protocol, BAIF aims to show that rigorous mathematical guarantees about real‑world code are achievable. This should encourage messaging providers and other safety‑critical software developers to adopt similar techniques, and help build the verification capabilities BAIF sees as essential for guaranteed‑safe AI systems.
Community Signal
Updated 05/18/26Endorsements support Beneficial AI Foundation (BAIF).
No endorsements yet.
Discussion
No comments yet. Be the first to share your thoughts.
Details
- Start Date
- Apr 20, 2026
- End Date
- -
- Expected Duration
- -
- Funding Raised to Date
- -