The WASM spec was developed with formal verification in mind, and the core specification, interpreter and type checker had mechanized safety proofs very early on [1]. This is backwards from how most bytecodes were designed, so that's very promising. Note also that the specification is an explicitly single-pass type checking, which is very efficient.

The difficulty of full safety verification on the JVM is well studied [2]. The security-focused Joe-E language actually decompiles JVM bytecodes back to Java to avoid the many full abstraction failures that have been documented.

The CLR is a little better on the safety record, but the verification costs can be even higher because the CLR supports various pointer types. Proper verification requires control-flow analysis, but instead they partition the bytecode into safe/unsafe variants and only the safe variant is "verifiable". IIRC, WASM doesn't have this limitation.

[1] https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif...

[2] http://www-master.ufr-info-p6.jussieu.fr/2005/IMG/pdf/leroy-...