WebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal speci

WebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2]. [1] https://webassembly.github.io/spec/core/valid/instructions.html https://webassembly.github.io/spec/core/valid/instructions.h... [2] https://github.com/es-meta/esmeta https://github.com/es-meta/esmeta