If you think correctness is only about memory safety, only then you can you can "focus your auditing and formal efforts on just those small unsafe blocks". And this is a core problem of Rust that people think they can do this.
Memory and concurrency safety need to be the first steps, because how can you analyze results when the computer might not have executed your code correctly as written?
my comment (and indeed in this entire comment chain) is within the context of memory safety. This should have been clear because of the focus on unsafe, which, compared to normal Rust, relaxes only memory safety.
Obviously if you want to get formal guarantees beyond that property, you have to reason about safe code also.
(Also, the comparison in this entire chain is against C, and the latter is better than Rust in this regard… how?)
Yes, this discussion is about memory safety, but this does not invalidate my argument. There is no point in only auditing your code with respect to memory safety, so the argument that you can simply ignore everything outside "unsafe" blocks is simply wrong.