Mechanising WebAssembly Well?
summary
Mechanization of WebAssembly focuses on two concrete routes: an extrinsic approach where preservation + progress yields an interpreter for free, and a dependently-typed "fancy" interpreter that bakes soundness into execution for stronger control and performance. Isabelle artifacts include a verified fast interpreter (used as a fuzzing oracle by the BigCode alliance), an optimized evaluation-context implementation and crash-classification proofs, microbenchmarks (Fibonacci) nearing non‑mechanized OCaml speed, and a WASM DSL that auto‑generates Isabelle/Coq/Lean definitions — auto‑proof generation remains open research.
AI-written summary · about
chapters (19)
- 0:00WebAssembly mechanisation intro
- 1:03Mechanising standards in Coq
- 4:15Verified WASM interpreter
- 6:01Old interpreter design
- 7:30Progress-preservation approach
- 11:27Fancy interpreter with soundness
- 13:11Simplest interpreter crashes
- 15:20Preservation with non-determinism
- 16:23Intrinsic vs extrinsic semantics
- 17:07Shared proof infrastructure
- 18:58Fibonacci benchmarks
- 21:11Mechanised proof challenges
- 21:53Embedding mechanisation
- 23:18Formal methods in standards
- 24:41New DSL for WASM
- 26:50Ryu’s WASM DSL project
- 27:55Isabelle Lean ACTA generation
- 28:55Future proof generation
- 29:17Summary
related talks
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
29mVerification of WebAssembly Features
01h 08mOn WebAssembly
01h 06mAs low-level as possible, but no lower
32mWebAssembly: birth of a virtual ISA
36mHelp me WebAssembly, You're My Only Hope
37mDecoding the hype behind WebAssembly: Looking under the hood
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)