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

Researchers have developed Signal Shot, a tool that uses the Lean theorem prover to formally verify the Signal protocol and its Rust implementation. This verification ensures the cryptographic security of the messaging protocol used by billions of people worldwide.