What other low-level format supports my points (a), (b), and (c)? And has an actual spec?

EDIT: you've since added some examples. Here are my (very subjective) opinions:

- The JVM isn't really all that low-level - it eeks out a lot of performance at runtime. Plus, you need to have GC, which tends to increase memory requirements and complicate real-time constraints.

- NaCL was interesting but its spec wasn't as good. IIRC Google didn't do too much in the way of asking for public input. I think some folks had some security concerns too. I really like WebAssembly's spec - I don't see any typing judgements or small-step rules for NaCL.

- Wasn't ANDF unix-bound?