Rust is not yet ready for formal verification, along with some ready libraries for that purpose, unlike Ada/SPARK. Hopefully, it will be there, just not yet. It still requires tremendous multi-year effort to finish that.
In addition to lacking formal verification tools, I'm worried about compiler certification with a language that changes as fast as rust, and c++, and even c now do. Yes you cannstick to a version, but the world and bug fixes, and libraries will pass you by. Which brings up another problem with rust for safety critical. The stdlib is so very thin, that doing almost anything requies a dependency tree of a dozen or more crates by different authors. You need to certify all those as well. Its a nightmare of an ecosystem from the safety cert perspective.
Many cases when you want cert will probably be nostd anyway so it is definitely worth pursuing given all the other advantages the language has. I'm just being grumpy because I love the language but I am a fan of batteries included languages. Or at least a thick stdlib and a boost-like thing. That is partly influenced by my primary dev environment being airgapped, and my secondary one being behind nexus/solarcube.
