The issue is not really about the verifiability of the bytecode but about the interpreter checking the invariants. JVM bytecode is intentionally designed to be verifiable so that the inner loop of the interpreter does not need to care about whether the operation is executed with correctly typed operands (which in the JVM case would be highly impractical and would essentially mean that you need twice the amount of memory). You can design a system where the bytecode is not verifiable, but instead the checks are done at runtime, CPython works that way.