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.
Nobody is arguing anything on the level of doing a full on Sel4 -- but
Sel4 does have generalized no memory leak, no uaf guarantees as a subset of all specification proofs, so my point "memory safely is possible to bolt onto even C" is still valid.
