You're not wrong, but formal verification is still useful for multiple reasons: 1. Cases where specification is much less complex than implementation, like pro

You're not wrong, but formal verification is still useful for multiple reasons: 1. Cases where specification is much less complex than implementation, like proving a sorting algorithm - the spec is very simple, forall integer i,j : i<j ==> result[i]<=result[j] plus the requirement that elements may not be removed or added 2. Ability to eliminate checks for improved performance (not sure if this applies to Rust yet, but it works great with Frama-C). 3. "Unit tests" for entire classes of behavior, not just specific inputs. Even if you cannot write a formal specification for a huge complex protocol, you can incrementally add asserts which cover much more area than simple unit tests.