Bringing the WebAssembly Standard up to Speed with SpecTec
summary
SpecTec is a DSL and toolchain that serves as a single source of truth for Wasm semantics, generating typeset spec prose, formal definitions, and a meta-level interpreter from one specification. The generated indirect interpreter passes 100% of applicable official tests. The pipeline auto-elaborates DSL to algorithmic and declarative forms, detects specification inconsistencies (it rediscovers historical bugs and finds ten new bugs across five proposals), and emits backends for docs, tests, and planned proof-assistant integration.
AI-written summary · about
chapters (10)
- 0:00WebAssembly and SpecTec intro
- 1:05WebAssembly standardization challenges
- 2:28SpecTec automation framework
- 3:33SpecTec workflow structure
- 6:53Algorithmic specs from DSL
- 9:45Bug prevention with SpecTec
- 11:35SpecTec correctness evaluation
- 12:59SpecTec summary and open source
- 13:43Extending SpecTec to JS APIs
- 14:47Future theorem assistant integration
related talks
26mSpecTec, a Single Source of Truth
55mGenerating Executable Specification from Formal Semantics of WebAssembly
01h 06mAs low-level as possible, but no lower
47m[Keynote] Keynote and SpecTec demo
29mVerification of WebAssembly Features
05mLighting talks and closing discussion
01h 08mOn WebAssembly
23mExperience Report: Stack Switching in Wasm SpecTec