There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.
I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
"Building High Integrity Applications with SPARK"
https://www.amazon.com/Building-High-Integrity-Applications-...
"Building Parallel, Embedded, and Real-Time Applications with Ada"
https://www.amazon.com/Building-Parallel-Embedded-Real-Time-...
"Embedded Software Development for Safety-Critical Systems"
https://www.amazon.com/Embedded-Software-Development-Safety-...
people were writing mission-critical C++ when C++ was new / only a few years old; with this in mind, rust is probably good to go with sufficient application/system testing
that said, since C++ & associated tooling exists, there is more of an opportunity cost since, in the context of today, there are more alternatives that could be considered