Assuming you mean seL4, that was formally verified by taking a manual specification of the L4 kernel and laboriously proving that the C code implements that spe

Assuming you mean seL4, that was formally verified by taking a manual specification of the L4 kernel and laboriously proving that the C code implements that specification. That is not at all what the compiler's lifetime/borrow check subsystems do for Rust. They know nothing about what the program is supposed to do; they only check that some relatively-simple rules are followed. That's why Rust requires so much less effort on the part of the programmer than formalisms that aim to prove programs correct.