Petr4 is a formal framework that models the semantics of P4. It consists of a clean-slate definitional interpreter for P4 and a formal calculus that models the essential features of the language.
Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus approximates target-specific behaviors using non-determinism.
The Petr4 interpreter was validated with a suite of over 750 tests from the P4 reference implementation, exercising the target interface with tests for different targets. The core calculus was validated with a proof of type-preserving termination.
Petr4 repository
