Book
Open access
Sep 2026
Welder: Compositional Liveness Verification of Cluster Control Planes
We present the first compositional approach to formally verifying cluster control planes such as Kubernetes. Control planes are large, distributed systems composed of interacting controllers with subtle liveness and safety dependencies. Our approach, Welder, emphasizes compositionality to make verification manageable a...
Zhi-Xiang Cai, Nikhil Date, J. Gu et al.
· Proceedings of the ACM SIGOP... · 1 citation