This is not about unsafe WASM which should be rejected by verifier. This is about the raw machine output that the compiler generates from WASM. As with JIT for JS currently nothing verifies WASM compiler output. So a bug in the compiler may result in a WASM that passes the verifier to be translated into unsafe machine code.

Same thing applies to NaCl verifier. Bugs in verifier can cause problems. Verification or generation bugs are bug, not security weaknesses in the architecture.

(I should not need to mention this but compiling is form of verification).

"Same thing applies to NaCl verifier. Bugs in verifier can cause problems. "

Not like with the other, though. You can statically verify NaCl stuff because it was designed for that to be easy. If WebAssembly doesn't do that, then it's a step down from NaCl at least on this risk. That it matters should be obvious given all the research by the kind of CompSci people that invented NaCl on eliminating that risk from the TCB. It's part of a larger concept where you make the things generating the risky code untrusted with the trusted checkers so simple they can be mathematically verified. Here's an example from a top group on NaCl:

http://www.cse.psu.edu/~gxt29/paper/rocksalt.pdf

I'm not worried about this too much as it will probably be some brilliant student's personal project in near future if it's not being researched already. A quick Google shows the Github has the full, C semantics with compiler (KCC) and a Javascript semantics at least has a prototype from 2015 of WebAssembly.

https://github.com/kframework/wasm-semantics

NaCl verifier in practice is much simpler than WASM compiler leading to a significantly reduced attack surface.

This is not true. NEXE has different security boundaries enforced differently on each supported platform. You need to write disassembler for each supported instruction set and verify them. This is more complex task than generating correct code from wasm.