I don't think this is as strong a claim here as you think. The point of unsafe is to point you toward the areas you need to audit. Unsafe code can't be proven

I don't think this is as strong a claim here as you think. The point of unsafe is to point you toward the areas you need to audit. Unsafe code can't be proven memory safe by the compiler [...but the rest can be]. It's far easier to audit 10 or 100 LoC of unsafe rust than 10 or 100 thousand of C++. And even in C++ there are subsets of the language that are supposedly memory safe. But even when writing in those subsets I'm not convinced that the abstractions I'm building on are as well validated as rust.