people often mention forcing refactoring/rewrites as a benefit of unit testing, that you end up with code that is actually better in testing-unrelated ways. thi

people often mention forcing refactoring/rewrites as a benefit of unit testing, that you end up with code that is actually better in testing-unrelated ways. this is true in my experience. i wonder how true this is of formal verification? especially in a language like Rust that has a fairly fancy type system?