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.
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]