Here's an article about the research on it which lays out the properties in simple terms: https://smallcultfollowing.com/babysteps/blog/2016/10/02/obs...
I'm curious why you think that statement is doing heavy lifting. It's much easier to write and verify that a few lines of code are correct than it is to write and verify that an entire program is correct. But that's the norm in C and Zig, and historically people haven't been very good at it. That's why we try to do it as little as possible.
Many more C programs have been verified than Rust programs. Also, Zig's spatial and memory safety is as good as Rust's, so it's not really similar to C at all.
The reason it's not "the norm" is that (especially with spatial safety taken care of), not every line is equally dangerous at all. Still, there's no doubt that more guarantees help, but that is only when all other things are equal. If you pick a low-level language for mostly low-level things, so Rust doesn't offer safety for the trickiest code, and furthermore it makes certain things harder to see because the language is more complicated, then things become much less clear. Obviously, when the vast majority of the trickiest, most important code doesn't need to be low-level, Rust would probably be safer on the whole, but in such situations I see no reason to choose either Rust or Zig. You need to choose a low-level language if the core of what you're doing needs to be low-level.
https://internals.rust-lang.org/t/language-vision-regarding-...
You must reason about the invariants in unsafe code on a global level. In particular, you could have unsafe code in crate A, whose data are then used by crate B. It could be fine. But then crate B changes its implementation which now violates the invariant expectations of crate A.