Signal Shot: a project to verify the Signal protocol and its Rust implementation using Lean

Signal and the Beneficial AI Foundation launched Signal Shot, a formal verification project using Lean to prove correctness of the Signal protocol and its Rust implementation. The project leverages Aeneas, a Rust-to-Lean translator developed by Son Ho at Microsoft Research, which translates Signal's actual code into provable Lean without requiring parallel maintenance. This moonshot demonstrates that Lean has matured from verifying pure mathematics to verifying deployed cryptographic software.