FWIW, with my contrarian hat firmly affixed, I suspect that C plus tools makes more economic sense than Rust. https://compcert.org/ https://compcert.org/ > Th

FWIW, with my contrarian hat firmly affixed, I suspect that C plus tools makes more economic sense than Rust. https://compcert.org/ https://compcert.org/ > The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. https://frama-c.com/ https://frama-c.com/ > Frama-C gathers several static and dynamic analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. https://www.cprover.org/cbmc/ https://www.cprover.org/cbmc/ > CBMC is a Bounded Model Checker for C and C++ programs. ... CBMC verifies memory safety (which includes array bounds checks and checks for the safe use of pointers), checks for ex­cep­tions, checks for various variants of undefined behavior, and user-specified as­ser­tions.