Real-world programming languages have multiple implementations and continue to evolve, often resulting in inconsistencies between implementations. To mitigate this issue, language mechanization frameworks have been proposed, which guarantee the same behavior between the executable semantics described in a mechanized specification and tools such as interpreters automatically generated from the mechanized specification. Recently, real-world programming languages have adopted mechanized specifications. The TC39 committee decided to integrate ESMeta into the CI systems of the JavaScript language specification and its official test suite. In 2025, the WebAssembly (Wasm) Community Group voted to adopt SpecTec for authoring future versions of the Wasm specification. Similarly, P4-SpecTec is being developed, targeting to be a specification authoring toolchain for the P4 language.

In this tutorial, we will discuss the challenges faced by each programming language community, how mechanization frameworks have addressed them, and how language community governance can facilitate adoption. This tutorial aims to provide a hands-on introduction to P4-SpecTec, as well as guidance for applying mechanized specifications to new programming languages.