Register to attend this P4 Developer Days webinar, “From Semantics to Software: Building a Verification Ecosystem for P4 using HOL4P4”
Date: September 25, 2025
Time: 8:00am Pacific
Abstract
We present a comprehensive formal verification ecosystem for the P4 network programming language, built upon HOL4P4, an abstract model of P4 execution embedded in the interactive theorem prover HOL4. The HOL4P4 formalization provides a semantics and a corresponding type system with formally verified progress, preservation, and type-soundness theorems. In addition, it has been validated using a test suite from the P4 reference implementation.
From this robust semantic foundation, we have developed multiple practical verification tools. Our proof-producing symbolic execution engine enables functional correctness verification of entire real-world P4 programs, with all results mechanically verified against the HOL4P4 semantics. Additionally, we present a formally verified P4 software switch that maintains correctness guarantees from source to binary by leveraging both HOL4P4 and the verified CakeML compiler. This switch integrates seamlessly with existing network testing frameworks like Mininet while demonstrating decent performance compared to existing similar solutions.
Together, these contributions demonstrate how rigorous formalization can serve as the foundation for a complete ecosystem of verification tools, bridging the gap between theoretical guarantees and practical network development while meeting the growing demand for formal assurances in critical network infrastructure.
Speaker
Didrik Lundberg combines academic research as a PhD candidate at KTH Royal Institute of Technology with practical engineering experience at Saab AB. He specializes in interactive theorem proving and formal verification, particularly for low-level and network-related systems. His current focus is developing tools based on the HOL4P4 formalization of P4.