[Dylan16807]

Unsafe blocks have to uphold their invariants while accepting any possible input that safe code can give them. Any subtle interactions enabled by "unsafe" need to be part of the invariants. If they don't do that, it's a bug in the unsafe code, not the safe code using it.

If done properly, you can and should write out all the invariants, and a third party could create a proof that your code upholds them and they prevent memory errors. That involves checking interactions between connected unsafe blocks as a combined proof, but it won't extend to "the rest of the program" outside unsafe blocks.