SpecTec, a Single Source of Truth
summary
SpecTec defines a single source of truth DSL for WebAssembly semantics that generates LATTE-style formal rules, restructured-markdown prose, an algorithmic interpreter, and targeted test suites, claiming automated consistency across artifacts. The tool finds real bugs in V8, SpiderMonkey, JavaScriptCore, Wasmtime and Wasmer, helped the WASM community group adopt SpecTec by vote, supports incremental replacement of manual spec text, and currently remains specialized to WASM with open limits (evaluation contexts, some numeric handling) and ongoing work.
AI-written summary · about
chapters (12)
- 0:00Workshop context
- 1:26SpecTec and adoption
- 2:50WebAssembly spec challenges
- 7:33SpecTec as solution
- 10:01How SpecTec works
- 13:34Automated spec artifacts
- 15:39WASM 3.0 features
- 16:20Bug detection with SpecTec
- 17:50Testing WASM engines
- 18:56Future directions
- 21:03Generalizing SpecTec
- 23:38Q&A
related talks
16mBringing the WebAssembly Standard up to Speed with SpecTec
25mP4-SpecTec: A Language Mechanization Framework for P4
23mExperience Report: Stack Switching in Wasm SpecTec
05mLighting talks and closing discussion
01h 02mProgramming Language Research for Technical and Social Good: What PL Can Do for Good?
24mMeta-tracing Interpreters in WebAssembly
25mExorcising Spectres with Secure Compilers
12mSpec-Tacular Streaming: Lessons Learned in Standards Land