The WebAssembly language specification is unusual compared to most industrial languages in that it defines a pen and paper formal model of language semantics. This formal model can be mechanised, that is, encoded to interactive theorem provers, and this mechanisation can then be used to prove properties about the language, such as type soundness, or to derive formally verified artefacts such as executable type checkers and interpreters. This has been demonstrated by the WasmCert-Isabelle and WasmCert-Coq projects, which are mechanisations of WebAssembly in Isabelle/HOL and Rocq interactive theorem provers.

We present the updated WasmCert-Isabelle mechanisation that covers WebAssembly 2.0. WasmCert-Isabelle previously mechanised WebAssembly 1.0 and some of the language extensions, such as the SIMD proposal and the multi-value proposal. The 2.0 version of WebAssembly introduced more extensions to the language, such as the bulk memory operations proposal and the reference types proposal. These additions, even though they are smaller than some of the ones that are planned for Wasm 3.0, still made substantial changes to the language: they added reference values and a set of new instructions, introduced subtyping rules for instruction sequences, and modified the Wasm runtime structure and instantiation procedure. The update of WasmCert-Isabelle needed a large refactoring that touched most of the mechanisation, requiring significant modifications to the type soundness proof, verified type checker, verified interpreter, and module instantiation procedure.

One of the verified artefacts in WasmCert-Isabelle is a formally verified WebAssembly interpreter that can be extracted to OCaml and which passes all of the tests in the WebAssembly test suite. Formally verified interpreters can be used to test non-verified WebAssembly engines in a differential random testing setting, as previously demonstrated by the WasmRef-Isabelle project, which builds on top of WasmCert-Isabelle to create a faster verified interpreter for Wasm 1.0 + SIMD extension and which was used as a fuzzing oracle for Wasmtime by the Bytecode Alliance. Although fuzzing oracles need not necessarily be as performant as industrial WebAssembly engines, their utility still depends on their speed, as a faster fuzzing oracle can achieve larger testing throughput with the same computational resources. We consider ways in which we could improve the performance of the verified interpreter without significantly increasing the verification burden. In particular, we explore how the interpretation of stateful operations on WebAssembly memories can be sped up by using different data structures to represent memories in the extracted OCaml code of the WasmCert-Isabelle interpreter.