WasmRef-Isabelle: how to formally verify a not-slow interpreter... - Maja Trela | Lambda Days 2024

CodeSync · March 14, 2025, 2:00pm

WasmRef-Isabelle: how to formally verify a not-slow interpreter… - Maja Trela | Lambda Days 2024

This talk was recorded at Lambda Days in June 2024. If you’re curious about our upcoming event, check https://lambdadays.org

Abstract
WasmRef-Isabelle is a WebAssembly interpreter written in Isabelle/HOL verified to be sound with respect to the WasmCert-Isabelle mechanisation of WebAssembly. Its main improvement on both the existing verified interpreter included in WasmCert-Isabelle and even the official (but unverified) WebAssembly reference interpreter is in performance – in fact, thanks to that, the Wasmtime (one of the main WebAssembly implementations) team adopted it as their fuzzing oracle.

So, how much direct effort does it take to achieve such a practical result in formal verification? Actually, not an insane amount. I’ll talk about how we verified WasmRef-Isabelle as a two-step refinement proof, using the WasmCert-Isabelle interpreter as the springboard so to speak, in a single (one-year) master’s thesis time.

Comments welcome! View the code-sync tag for more Code Sync talks!