ZENITH: Towards a Formally Verified Highly-Available Control Plane#
SIGCOMM 2025 digest Program Adjacent pick Coimbra · 8–11 September 2025
Pooria Namyar et al. (USC, Google)
Why: The "correct-by-construction vs. periodic reconcile" argument maps directly onto Kubernetes-style controller design the PM will recognize.
What: A microservice SDN controller that avoids state inconsistency by design, machine-verified, resolving inconsistencies 5x faster than reconciliation-based designs.
How: A formally verified specification with code auto-generated from it, plus abstractions letting developers independently verify SDN apps.
Where applicable: SDN control planes; the design philosophy generalizes to any reconciler-based system.