Ada was mandated by the DoD for a bit. My understanding is that, in practice, this involved making a half-hearted effort in Ada, failing and then applying for a variance to not use Ada.
In theory, something like Rust could do the job instead, but they'd still have to verify the entire chain. Rust is for the rest of us to get something half as reliable as that while also being able to write more than two lines of code per day.