Verification of WebAssembly Features
summary
A mechanized WebAssembly semantics exists in Isabelle mechanization and parallel mechanizations target Rock/MetaRoc, with proven preservation and progress for translations; an efficient interpreter extracted from the model is already used as a Wasmtime fuzzing oracle. Work formalizes Spect’s animation procedure (turning inductive specs into executable functions) in MetaRoc, identifies that Spect currently cannot auto-generate a type checker, and plans to extend Spect for the relaxed memory model and a shared‑everything threads design for concurrency.
AI-written summary · about
chapters (11)
- 0:00WebAssembly verification intro
- 1:49Formal WebAssembly history
- 5:32Womsert to Specttech
- 9:51Isabelle/Rocq mechanization
- 13:55Monomorphization and type families
- 16:23Specttech DSL demo
- 19:01Verified interpreters and Spect
- 20:24Spect animation verification
- 21:47Spect meta-theory critique
- 25:17WebAssembly concurrency
- 28:07Future for Spect and WASM
related talks
30mMechanising WebAssembly Well?
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
16mBringing the WebAssembly Standard up to Speed with SpecTec
01h 08mOn WebAssembly
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
01h 06mAs low-level as possible, but no lower