Lean"Can we prove that Signal's cryptography is secure — not just on paper, but in actual code?"
Signal Shot, launched today at the Software Verification in Lean workshop in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. A joint effort of Signal, the Beneficial AI Foundation, and the Lean FRO.
Open to contributions from anyone working on software verification, cryptography, protocol design, Rust, or Lean.