我们让 Agent 自动写出了 6000 行 TLAPS 证明

最近我们在分布式协议形式化验证上推进了一步：在此前分布式协议归纳不变式自动推导工作的基础上，我们进一步借助 agentic harness，实现了 TLAPS 证明脚本的自动化生成。本文主要讨论的是自动生成 TLAPS 证明脚本。

更具体地说，对于 MongoLoglessDynamicRaft 这个级别的协议，我们已经能够把链条打通到：

自动生成归纳不变式 -> 自动书写 TLAPS 证明 -> 证明安全性质

这里最值得强调的一点是：TLAPS 证明部分没有插入任何协议特定的人工提示或手写 lemma。Agent 看到的是协议、归纳不变式、证明目标和通用证明反馈；之后，它通过反复推进 proof obligation，最终写出了完整证明。

这份证明草稿总共 6308 行 TLAPS 代码，全部由 agent 生成。

证明文件链接：

MongoLoglessDynamicRaft_IndAuto_ProofDraft.tla

背景：为什么这件事难

分布式协议的安全性证明通常要跨过两道门槛。第一道是找到足够强的归纳不变式，这本身就很难，因为协议设计者需要从大量状态和执行路径里找出一组条件：它既要强到足以推出安全性质，又不能被任何一步协议动作破坏。第二道是把这些不变式写成 TLAPS 能检查的机械化证明，这通常更耗时：证明需要拆成大量细小的 proof obligation，并逐一补齐前提、定义展开和中间推理。过去，如果协议设计者想把一个真实协议的安全性质形式化证明出来，往往需要投入很长时间在这两件事上。这次结果是在自动生成归纳不变式之后，继续自动生成 TLAPS 能检查的证明脚本。

这次做了什么

这次实验的目标协议是 MongoLoglessDynamicRaft。它不是一个玩具协议：它包含动态配置、term、server state、配置传播等机制，已经足够体现真实分布式协议证明中的结构复杂度。

我们首先使用此前工作自动得到 MongoLoglessDynamicRaft 的归纳不变式。随后，我们把协议、归纳不变式和证明目标交给一个 agentic harness，让 agent 自动完成 TLAPS 证明书写。

整个 TLAPS 证明生成过程可以概括为三步：

前提插入：agent 根据当前 proof obligation，识别需要显式引入的协议定义、类型约束、动作前提和已知不变式。
证明骨架搭建：agent 按 action 和 clause 搭建证明骨架，将归纳证明拆成可逐步推进的局部证明任务。
Obligation 推进：agent 调用 TLAPS 检查当前证明，读取失败信息，再针对未完成的 obligation 补充更细粒度的中间步骤，直到证明通过。

重要的是，这个过程不是为 MongoLoglessDynamicRaft 手写的一套证明策略。Harness 并不包含该协议的特殊知识，也没有人工塞入“这里应该用某个协议专属 lemma”之类的信息。Agent 依靠通用的证明反馈循环，一步步把证明补齐。

结果

最终生成的证明文件是一个完整的 TLAPS proof draft：

MongoLoglessDynamicRaft_IndAuto_ProofDraft.tla

文件总计 6308 行。证明被拆成了很多小步骤：先说明协议中变量、配置和状态转换需要满足的基本事实，再按协议动作和 invariant clause 逐个证明，说明每一步执行之后自动生成的归纳不变式仍然成立，最后由这些不变式推出目标安全性质。

这里关键的不是某一个局部证明步骤有多复杂，而是 agent 能够持续生成并修复大量证明步骤，把它们组织成一个完整、可检查的 TLAPS 证明文件。

还没有解决什么

目前我们证明的是 MongoLoglessDynamicRaft 这个级别上，从归纳不变式自动生成到 TLAPS 证明自动生成的链条。不同协议的状态空间、动作结构、不变式形态和证明风格都可能不同。后续还需要在更多协议上检验这种方法的稳定性，尤其是包含更复杂日志结构、更复杂安全不变式，以及需要更深组合推理的协议。

从工程角度看，目前还有三个现实问题：token 消耗仍然偏高，证明状态还需要更充分地持久化和复用，证明闭合速度也还有待加快。接下来我打算进一步优化 harness 脚本和相关持久化内容，让 agent 不必每轮都重新理解全部上下文，而是能在结构化的证明状态上继续推进，并更快定位和补齐尚未闭合的 proof obligation。