constructs must leave the stack at the same height with the same types
That's easy to 'document' and harder to do. It's what the JVM did, again, in the 90s. Now the verifier chapter in the JVM spec is now about 160 pages long.
We learned our lessons from the JVM, and the verification algorithm for WASM is vastly simpler. It's even been formalized and fits in about 3/4 a page.
Sadly it is more complicated - but the document in the link was written before a bunch of problems were found (with things like unreachable code, which is indeed trickier in stack machines than ASTs).
(Those problems and their solutions haven't been documented yet AFAIK.)
Why? This document suggests that it's not that different.
"The main new changes to verification are:
- All branches to the end of a block must have the same arity and same types, including the implicit fall-through to end.
- The true block of if-end constructs must leave the stack at the same height as when the if was entered.
- The true and false blocks of if-else-end constructs must leave the stack at the same height with the same types."