Every language has operational semantics; they just may not be well specified, but from what I can tell, the Ethereum VM bytecode has a pretty good spec. However, well-defined semantics are just necessary for formalization. They cannot ensure correctness just as the clear operational semantics of Turing machines don't help ensuring the correctness of every Turing machine program. You still need a tool that will help you reason about a program, given its language's semantics.
Ron