> any embedded work or kernels Perhaps not, but in a kernel you'd have plenty of your own unsafe code. SEL4 doesn't. There are, of course, people thinking ab

> any embedded work or kernels 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 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.