NaCL verifier is just a loop that essentially matches the instructions against a white list and checks their format and offsets. WebAssembly needs parser/linker/optimizer/assembler. Granted that the format is optimized for fast translation, but just the amount of code to support data structures in the implementation like maps, lists etc. must be big.

NaCL also needs those things because it has to compile it's bytecode to machine code on multiple architectures. It's no different than webasm, just a different bytecode. A big advantage of webasm is that it's integrated into the existing javascript VM, that has already been sandboxed and battle hardened.

I believe that's PNaCl. NaCl just handles already-compiled machine code. But of course NaCl isn't portable, which is why PNaCl exists.

As in my other comment, something like that can be mathematically verified for correctness as well. That requires simplicity if one doesn't want to throw person-years of work at it w/ possibility of finding out it was impossible. My comment links to a formally-verified checker for NaCl as well.

https://news.ycombinator.com/item?id=14460649