WasmRef-Isabelle: How to Formally Verify a Not-Slow Interpreter

Explore the development of WasmRef-Isabelle, a WebAssembly interpreter written in Isabelle/HOL that's formally verified for soundness against the WasmCert-Isabelle mechanisation. In this 19-minute conference talk from Lambda Days 2024, Maja Trela explains how this interpreter significantly outperforms both the existing verified interpreter in WasmCert-Isabelle and the official (unverified) WebAssembly reference interpreter. Learn how the Wasmtime team adopted WasmRef-Isabelle as their fuzzing oracle due to its performance advantages. Discover the surprisingly manageable effort required to achieve practical results in formal verification, as Trela details the two-step refinement proof process completed during a one-year master's thesis timeframe.