The challenge of compiling for verified architectures

Presently all found speculation bugs have been promptly addressed in BPF while Wasm implementations continue to hope. Yes, this difference is poorly defined and probably cannot be formalized. Yet it is clear that it is affected by the nature of checks that has to be done at runtime.