P4-SpecTec

P4-SpecTec is a mechanization toolchain for the P4 programming language. It provides a domain-specific language for writing formal specifications in the form of algorithmic inference rules (Lee et al., 2026).

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 a specification written in P4-SpecTec.

In this chapter

• Installation: how to build and install P4-SpecTec
• Basics: the core syntax and constructs of P4-SpecTec
• Toolchain Pipeline: how the toolchain compiles a spec and a program, then runs one against the other
• Commands: the nano-p4spectec subcommands and their flags
• Standard Library: the built-in utility functions used throughout the spec