EDIT: And when I mean formally define, I mean something that is machine-checkable so implementations would have a conformance suite.
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.
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.