I believe someone is building something like that on top of sel4, which gives even stronger correctness guarantees than Rust, even though it's C.