Unfortunately, it's not. Now I do think it will be eventually fixed, but given how long it has taken it must be thorny. https://github.com/rust-lang/rust/issues/25860
There has also not been a single case of this bug being triggered in the wild by accident.
There was a Git repository demontrating unsoundness issues in the compiler, but I seem to be unable to find it anymore :/. It seemed like there would be more than one underlying issue, but I can't really remember that.
Per https://blog.rust-lang.org/2023/01/20/types-announcement.htm... there is a roadmap for ensuring Rust type system soundness end of year 2027. I think it means the implementation.
But this time I've starred and cloned it!
I didn't quite see if this actually exploits multiple bugs or leverages just one, though.
The only language with such a proof that I am aware of is StandardML. Even OCaml is too complex for a soundness proof.
In C, the type system does not express things like pointer validity, so you have to consider the system as a whole every time something goes wrong. In Rust, because the type system is sound, you can consider each part of the program in isolation, and know that the type system will prevent their composition from introducing any memory safety problems.
This has major implications in the other direction as well: soundness means that unsafe code can be given a type signature that prevents its clients from using it incorrectly. This means the set of things the compiler can verify can be extended by libraries.
The actual practice of writing memory-safe C vs memory-safe Rust is qualitatively different.