79. 修复一个经过形式化验证的垃圾回收器的证明

他们做了什么

Codex 可以访问仓库，编辑 Rocq 证明文件，运行有针对性的 make 构建，并通过一个 rocq-mcp 服务器查看证明状态。它先修复了 VST 相关的证明，然后是图同构定理。它提出了"记录反向边"的不变式，由作者进行审核。作者要求在修改任何 Definition 之前必须先讨论，并拒绝在没有证据的情况下增加新的 VST 前置条件。

结果如何

这个分支编译通过，并作为第 30 号 PR 合并到上游。主定理于 4 月 29 日被接受，之后的一次审查删除了一个过时的"无反向边"前提。这只是一个个例，并非对照研究。

需要知道

要做好大量监督的准备：十天里，Codex 共活跃运行约 59 小时，人发出了 415 条提示，工具调用达 13,305 次，而且没有测得明显的提速效果。

你可以这样尝试

在我位于 [文件夹] 的 [Coq/Lean/Isabelle] 项目中，[我做的改动] 之后，证明 [文件或引理] 出错了。编辑文件、运行构建，并以最小的局部改动修复证明。未经询问，不要削弱或修改任何规格或不变式；最后列出你修改过的每一条陈述，方便我审核。