Hi!
We are happy to announce the first public release of p4spectec, a framework for mechanizing the P4 language specification. It provides a domain-specific language for writing formal specifications in the form of algorithmic inference rules (Lee et al., 2026).
A specification written in P4-SpecTec is executable. By writing typing rules with P4-SpecTec, you get a reference type checker. By writing dynamic semantics rules, you get a reference interpreter. The prose backend also generates human-readable documentation from the mechanized specification.
For detailed instructions, source code and the mechanized P4 specification, check out the GitHub repository linked to the package.