Projects like Ferrocene or GNAT Pro seem to indicate that's a possibility. (automotive gaining traction sort of paves the way to avionics/aerospace).
https://ferrocene.dev/en/ https://www.eenewseurope.com/en/first-rust-compiler-qualifie...
I don't know a lot about Rust myself, but the impression I get is that it is a bit less obviously deterministic than C.
Things boil down to (IMHO): - every requirement must be traceable to code - every line of code must fulfill a requirement - any dynamic behavior (for example heap allocation) must be proven to work under all circumstances