Abstract

Today, large-scale software-defined networks use microservice-based controllers. Bugs in these controllers can reduce network availability by making the data plane state inconsistent with the high-level intent. To recover from such inconsistencies, modern controllers periodically reconcile the state of all the switches with the desired intent. However, periodic reconciliation limits the availability and performance of the network at scale. We introduce Zenith, a microservice-based controller that avoids inconsistencies by design rather than always relying on recovery mechanisms. We have formally verified Zenith's specifications and have proved that it ensures the network state will eventually be consistent with intent. We automatically generate Zenith's code from its specification to minimize the likelihood of errors in the final implementation. Zenith's guarantees and abstractions also enable developers to independently …

Date

September 8, 2025

Authors

Pooria Namyar, Arvin Ghavidel, Mingyang Zhang, Harsha V Madhyastha, Srivatsan Ravi, Chao Wang, Ramesh Govindan

Book

Proceedings of the ACM SIGCOMM 2025 Conference

Pages

409-433