Anvil 团队组合式形式化验证 Kubernetes 控制平面

tianyin_xu · x · 2026-09-21

Xu Tianyin 介绍由 @Catoverflow 与 @xudongsun 领导的 Kubernetes 控制平面形式化验证工作。团队提出组合式验证方法 CORE（COmpositional REconciliation），复用原 Anvil 的 ESR 规约来描述各控制器的 reconcile 逻辑，并用 rely-guarantee 条件约束控制器间干扰，同时编码活性与安全性。这展示了一条渐进式验证大型控制平面的可行路径：先逐一验证单个控制器，再组合成整体证明。论文在规约设计、证明与实现层面都有大量可借鉴的细节。