But metadata is needed for proper formal reasoning, and C has barely any additional information content over some very vague “typing” hints, everything else being only conventions enforced more or less by the linux community.

So Rust’s lifecycle annotations are what makes proper proofs possible in the first place.

(As for proofs though, they are no silver bullets either — a program of linux’s complexity is unlikely to be ever completely verified, but rust may indeed give valuable guarantees for most of the program)