Perhaps not, but in a kernel you'd have plenty of your own unsafe code.
SEL4 doesn't.
There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute.
But you're right that bugs in the compiler could produce safety issues.