  WebAssembly (Wasm) is a low-level bytecode language and virtual machine,
intended as a compilation target for a wide range of programming languages,
which is seeing increasing adoption across diverse ecosystems. As a young
technology, Wasm continues to evolve -- it reached version 2.0 last year and
another major update is expected soon.
  For a new feature to be standardised in Wasm, four key artefacts must be
presented: a formal (mathematical) specification of the feature, an
accompanying prose pseudocode description, an implementation in the official
reference interpreter, and a suite of unit tests. This rigorous process helps
to avoid errors in the design and implementation of new Wasm features, and
Wasm's distinctive formal specification in particular has facilitated
machine-checked proofs of various correctness properties for the language.
However, manually crafting all of these artefacts requires expert knowledge
combined with repetitive and tedious labor, which is a burden on the language's
standardization process and authoring of the specification.
  This paper presents Wasm SpecTec, a technology to express the formal
specification of Wasm through a domain-specific language. This DSL allows all
of Wasm's currently handwritten specification artefacts to be error-checked and
generated automatically from a single source of truth, and is designed to be
easy to write, read, compare, and review. We believe that Wasm SpecTec's
automation and meta-level error checking will significantly ease the current
burden of the language's specification authors. We demonstrate the current
capabilities of Wasm SpecTec by showcasing its proficiency in generating
various artefacts, and describe our work towards replacing the manually written
official Wasm specification document with specifications generated by Wasm
SpecTec.
