lean

Signal Shot is a major formal verification initiative to verify the Signal protocol and its Rust implementation using Lean, combining advances in Rust-to-Lean translation (Aeneas), mathematical foundations (Mathlib/CSLib), automated tactics (grind/SymM), and AI-assisted formalization. This represents a significant test of whether Lean can scale from pure mathematics to deployed real-world software systems.