Software stack and toolchain for building and running software middleboxes that are guaranteed to be correct, while providing competitive performance and preserving developer productivity. With Vigor, developers write the middlebox code (i.e., the software network function, or NF) in C atop a standard packet-processing framework, putting persistent state in data structures from a Vigor-provided library. Vigor then automatically verifies that the resulting software stack correctly implements a specification (written in Python).