Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
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.
