Signal Shot: Verifying the Signal Protocol and Rust Implementation with Lean

8 hours ago

Signal Shot is a public moonshot to verify the Signal protocol and its Rust implementation using Lean, focusing on actual code rather than theoretical math.
It is a collaboration involving Signal, the Beneficial AI Foundation, and the Lean FRO, inspired by the Liquid Tensor Experiment which demonstrated Lean's scalability for modern mathematics.
Key components enabling this effort include Aeneas (a Rust-to-Lean translator), Mathlib and CSLib (Lean libraries for math and computer science), grind and SymM (verification tools), and AI assistance for autoformalization and routine tasks.
SymM, a new monadic framework for software verification developed by Lean FRO, offers significant speed improvements and scalability, crucial for handling verification conditions efficiently.
The project relies on Lean's small, sound kernel with independent implementations to ensure proofs are verifiable without trust in the authors, serving as AI safety infrastructure.
Signal Shot is open for contributions from experts in software verification, cryptography, protocol design, Rust, and Lean, with needs in libraries, tool scaling, and cryptographic review.
An update on progress is scheduled for the Lean Paris Hackathon on April 20, 2026, aiming to prove Lean's scalability for deployed software, similar to LTE's impact on mathematics.

Hasty Briefsbeta