Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes.

The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4.

As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.