Welder 论文亮相 SOSP：用形式化验证迈向验证 Kubernetes 级集群控制面

Welder 论文将在 SOSP 大会 Verification and Formal Methods 分场展示，目标是验证 Kubernetes 等大规模集群控制平面，这是该长期目标的第二步。一作 Catoverflow 称这是其博士阶段第一个严肃研究项目，目前 Welder 中已验证的控制器还相对简单。作者把形式化验证与 AI agent 能力提升联系起来，认为手工构造证明并不有趣。