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.
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?)