WebAssembly is a rapidly evolving binary format originally designed for efficient and safe execution of low-level languages like C and Rust on the web supported by all major browsers. Since its release in 2017, it has expanded to diverse execution environments and has grown extensively in its features. The importance of the language and its design with a formal specification makes it a compelling subject for programming languages and formal verification research.

This thesis focuses on my contributions to studies around the WebAssembly semantics and verification. I contributed a major part in the WasmCert-Coq mechanisation of the WebAssembly in Coq, starting from its inception which drew definitions from Watt's Isabelle/HOL mechanisation for a pre-1.0 version of WebAssembly, until my update of the semantics to Wasm 2.0 and beyond, which also produces a fully conformant interpreter as its extracted artifact. My work on the WebAssembly mechanisation has discovered and helped fix several errors in the WebAssembly specification, fulfilling the promise of the language mechanisation for refining an important non-mechanised specification.

In addition, through my work on WebAssembly mechanisation, several methods have been explored and implemented to reduce the effort of maintaining mechanised models of WebAssembly. In particular, my work on the progressful interpreters proposes a new method using a dependently-typed design to merge the interpreter, its correctness, and the progress property into one mechanisation artifact.

Besides designing the mechanisation of WebAssembly’s semantics, I demonstrated the usefulness of language mechanisation to the formal verification by jointly developing the Iris-Wasm program logic using the Iris separation logic framework, which supports modular reasoning about WebAssembly programs, including host-WebAssembly interactions and module instantiation.

My efforts provide a foundation for efficient, scalable, and reliable verification of WebAssembly as it continues to evolve, ensuring its role as a secure and efficient platform for modern computation.