Interesting, how common is this vs just unit testing? How do you avoid formally verifying something against a spec that could subtly fail in production?
Something like TLA+[1] and Quint[2] specifications can be verified for correctness using Apalache[3]. Then test the Rust code against the specifications using quint_connect.[4]