> That is the soundness guarantee, it cannot get stronger than that as the langauge allows down casts, and those are fundamentally unverifiable at compile time.

An explicit downcast is allowed to fail at runtime. But if you can get a runtime cast failure in code that did not contain any cast, that's a soundness bug.