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

Sure, this will be very cool, but I am unsure what is so groundbreaking about it. Didn't Project Everest prove TLS at the code level?