The P4 programming language enables modeling the behavior of the network data plane in software. With increasingly powerful and complex applications running in the network, the risk of errors also increases, especially, since P4’s main abstraction for representing packet data lacks basic safety guarantees. This reinforces the need for methods and tools to statically verify the correctness of data plane programs. Existing data plane verification tools employ closed-world monolithic reasoning. However, dataplane progamming languages have begun to specify rich packet-processing functionality by composing simple functions defined in reusable libraries. Verifying such composable functionality requires compositional reasoning tools. Type systems are a lightweight compositional verification technique that features modular reasoning. However, there is a significant gap between guarantees provided by verification tools like p4v and those provided by type checkers based on traditional typing disciplines like SafeP4, which cannot reason about runtime values. In this paper, we close this gap by presenting Pi4, a dependently-typed variant of P4 based on regular types with decidable refinements. We prove soundness for Pi4’s type system and present case studies illustrating Pi4’s ability to check realistic program properties.