Signal Shot
Join us from April 20, 2026, to formally verify the Signal protocol and Signal app with Lean
UPDATES
> Apr 20, 2026: Signal Shot Launch and Talk by Max Tegmark at Software Verification in Lean workshop in Paris — see blog post and Lean FRO blog post
> Apr 13, 2026: Signal Shot Pre-Launch at Rust Verification workshop in Torino
> Apr 1, 2026: Signal Shot Pre-Launch with our Collaborators
OBJECTIVES
Develop tools, not just for end-to-end machine-checking the full protocol stack, but also for designing new protocols and for continuous verification as the software evolves. Create a reference for how verified software should be shipped.
Catalyze software verification in Lean, improve required tooling and performance, and bring together the Lean verification ecosystem. Connect recent improvements in AI-assisted formalization and theorem proving to software verification.
Build capabilities for AI safety by scaling up software verification through a combination of AI tools, open-source software tools and open standards. Fuel a virtuous cycle: better AI tools driving formal verification adoption, which in turn produces more verified code to train still better AI tools.
WHY NOW?
The broad availability of increasingly capable AI-powered hacking tools makes this project very timely.
MOONSHOT STAGES
We will accomplish the technical goals in stages. For more information, please read our launch post.
HOW TO CONNECT
Please create a Zulip account and join this channel to receive updates about Signal Shot.
HOW TO CONTRIBUTE
We welcome contributions! Whether you're experienced with formal verification or just learning, there are ways to help:
Add specifications to unverified functions
Complete proofs for existing specifications
Improve documentation
Report issues or suggest improvements
Please visit the following GitHub repo for further instructions:
RESPONSIBLE DISCLOSURE
If you've found a security vulnerability in Signal, please report it via email to security@signal.org. Please only use this address to report security flaws in the Signal application. Signal does not have a bounty program, but does investigate security flaws reported to this address. For questions, support, or feature requests, please submit a support request or join the unofficial community forum.
STEERING CO-CHAIRS
Max Tegmark
President at the Beneficial AI Foundation
Meredith Whittaker
President at the Signal Foundation
Leonardo de Moura
Senior Principal Applied Scientist at AWS
Chief Architect of Lean FRO
ORGANIZING CO-CHAIRS
Shaowei Lin
Chief Scientist at the Beneficial AI Foundation
Rolfe Schmidt
Research Engineer at Signal
ORGANIZING COMMITTEE
Sofia Lanfri
Signal Challenge Project Coordination
Program Director at Beneficial AI Foundation
Mikhail Asavkin
Signal Challenge Platform Coordination
Product Manager at Beneficial AI Foundation
Armin Vrevic
Signal Challenge Tech Coordination
Sr. Engineering Manager at Beneficial AI Foundation
Thiago Silva
Signal Challenge Community Coordination
Sr. Manager at Beneficial AI Foundation
Oliver Butterley
Signal Challenge Science Coordination
Deputy Chief Scientist, Beneficial AI Foundation
Filippo A. E. Nuccio
Signal Challenge Formalization Coordination
Research Scientist, Beneficial AI Foundation
ORGANIZERS
COLLABORATORS
Karthik Bhargavan, Cryspen
Clark Barrett, CSlib, Stanford
Alexandre Rademaker, CSlib, Atlas Computing
Ilya Sergey, VERSE, NUS
Linard Arquint, VERSE, NUS
Mike Dodds, Galois, Inc
Vladimir Gladshtein, VERSE, NUS
Dawn Song, UC Berkeley