Congratulations to friends and colleagues Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner, whose paper “Two mechanisations of WebAssembly 1.0” has been accepted at the 24th International Symposium of Formal Methods (FM21).
WebAssembly (abbreviated Wasm) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. Wasm is unusual in that it is officially specified through a formal semantics. The paper introduces two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm’s compact design and official formal semantics enables the mechanisations to be particularly complete and close to the published language standard. The paper presents a high-level description of the language’s updated type soundness result, referencing both mechanisations and also describes the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.
FM21, which was planned to take place at the Institute of Software, Chinese Academy of Sciences in Beijing, China on 20-26 2021, will in the end be held online this year.