Microsoft Research has numerous languages that provide many, many more guarantees than Rust. If Microsoft were to design a completely new kernel, I'd be fairly disappointed if they didn't do it in something Z3 Boogie based like Dafny.