A decent amount of mission-critical software undergoes formal verification, like spacecraft flight software (my area of expertise). SparkADA lives on because of not just its safety, but formal verifiability.
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?
Make sure the specifications can’t fail by verifying them for correctness.
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]