p4cherry is an open-source P4 type checker and interpreter aimed at providing both a formal and executable model of the P4 language. Building on the foundational work of Petr4, p4cherry brings its clean-slate, modular design up to date with P4 version 1.2.4. Formally, p4cherry’s structure closely mirrors P4’s surface syntax and can be abstracted into a formal calculus. It supports nearly all core language features and is designed to aid in reasoning about P4 programs. As an executable tool, p4cherry has been validated against over 1,000 tests from the P4 reference compiler (p4c). It offers near-complete support for the V1Model architecture and limited support for eBPF. A web interface is also provided for easy experimentation and debugging. p4cherry can be used to compare the expected behavior of a P4 program as defined by the language specification and with the behavior exhibited by the reference compiler. (repo: https://github.com/kaist-plrg/p4cherry)
