This dissertation gives semantics to P4, a domain-specific language for describing packet processing in packet-switched computer networks. Additionally it describes verification tools for checking the equivalence of P4 programs. These verifiers can be used to check that a P4 compiler has not introduced bugs into programs while optimizing them. The verification methodology combines manual proof in an LCF-style proof assistant with automatic decision procedures that rely on SAT/SMT solvers for a compact trusted computing base.