Reasoning about network programs is challenging because of how they divide labor: the control plane computes high level routes through the network and compiles them to device configurations, while the data plane uses these configurations to realize the desired forwarding behavior. In practice, the correctness of the data plane often assumes that the configurations generated by the control plane will satisfy complex specifications. These specifications are either missing or maintained in complex English language documents, which makes correctly configuring devices hard. This thesis tackles this problem from three angles. First, we present algorithms for computing control plane interface specifications that ensure the safety of the data plane. These specifications can be used to improve the safety and quality of both the control plane and of the data plane. Then, we show how to automatically generate configurations for data plane programs, and finally, we conclude with a semantic framework for programming and relational verification of pairs of configurable programs.