WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly

Watch a 17-minute video presentation from the PLDI 2023 conference introducing WasmRef-Isabelle, a verified monadic interpreter for WebAssembly. Learn how this Isabelle/HOL-based interpreter, proven correct against the WasmCert-Isabelle mechanization, has been adopted as a fuzzing oracle in Wasmtime's continuous integration. Discover how WasmRef-Isabelle achieves both performance and specification correspondence, outperforming the official reference interpreter while maintaining correctness through a mechanized proof. Explore the two-step refinement proof process, performance comparisons with other interpreters, and extensions to WasmCert-Isabelle that enhance its utility as a fuzzing oracle. Gain insights into theorem proving, refinement techniques, and virtual machine implementation for WebAssembly.