> And a bug in one crate can cause UB in another crate if that other crate is not designed well and correctly.

Yes! Failure to uphold invariants of the underlying abstract model in an unsafe block breaks the surrounding code, including other crates! That's exactly consistent with what I said. There's nothing special about the stdlib. Like all software, it can have bugs.

What the proof states is that two independently correct blocks of unsafe code cannot, when used together, be incorrect. So the key value there is that you only have to reason about them in isolation, which is not true for C.

I think you're misunderstanding GP. The claim is that the only party responsible for ensuring correctness is the one providing a safe API to unsafe functionality (the upstream dependency in GP's comment). There's no claim that upstream devs are infalliable nor that the consequences of a mistake are necessarily bounded.

Those guys were writing a lot of unsafe rust and bumped into UB.

I sound like an apologist, but the Rust team stated that “memory safety is preserved as long as Rusts invariants are”. Feels really clear, people keep missing this point for some reason, almost as if its a gotcha that unsafe rust behaves in the same memory unsafe way as C/C++: when thats exactly the point.

Your verification surface is smaller and has a boundary.