Two mechanisations of WebAssembly 1.0

WebAssembly (Wasm) is a new bytecode language supportedby all major Web browsers, designed primarily to be an efficient com-pilation target for low-level languages such as C/C++ and Rust. It isunusual in that it is officially specified through a formal semantics. Aninitial draft specification was published in 2017 [14], with an associatedmechanised specification in Isabelle/HOL published by Watt that foundbugs in the original specification, fixed before its publication [37].The first official W3C standard, WebAssembly 1.0, was published in2019 [45]. Building on Watt’s original mechanisation, we introduce twomechanised specifications of the WebAssembly 1.0 semantics, writtenin different theorem provers: WasmCert-Isabelle and WasmCert-Coq.Wasm’s compact design and official formal semantics enable our mecha-nisations to be particularly complete and close to the published languagestandard. We present a high-level description of the language’s updatedtype soundness result, referencing both mechanisations. We also describethe current state of the mechanisation of language features not previouslysupported: WasmCert-Isabelle includes a verified executable definitionof the instantiation phase as part of an executable verified interpreter;WasmCert-Coq includes executable parsing and numeric definitions ason-going work towards a more ambitious end-to-end verified interpreterwhich does not require an OCaml harness like WasmCert-Isabelle