You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"

But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.