Over the last 5+ years, the P4 Team at Google has pioneered a paradigm that leverages P4 to improve the reliability, agility, and optionality of our data center networks. We view P4 programs as specifications, each capturing the precise requirements for a switch in a specific deployment role. We have developed automated tools that ensure that a given switch correctly implements a given P4 specification (with high probability).