Ethereum is like a real world PVP system fought with real money. And I wouldn't have it any other way.
How it ever got moved to prod is beyond me.
EDIT: And when I mean formally define, I mean something that is machine-checkable so implementations would have a conformance suite.
WASM couldn't be ported over to Ethereum because it isn't, so eWASM is being developed as the deterministic subset of WASM, for possible use in Ethereum.
I get the impression from their documentation (https://developers.cardano.org/en/virtual-machines/iele/abou...) that it's intended to address that, but I'm no expert in this area.
I actually hadn't considered this issue at all until you mentioned it, but was aware that one of Cardano's selling points is a focus on verifiability (e.g. via their Haskell-based Plutus language for smart contracts), and came across this IELE after a quick search through their materials.