验证过的垃圾收集器的修复正式证明

Codex能够编辑文件并运行构建以修复CertiGC证明；其本地修复功能表现良好，但仍需人工检查其不变量是否符合规范。

具体怎么做

Codex能够访问存储库，编辑Rocq证明文件，执行指定构建，并使用rocq-mcp服务器检查证明状态。它首先修复了VST证明，然后处理图同构定理。它提出了记录回溯边不变量，作者对其进行了审核。任何定义更改前都需要讨论，且在没有证据的情况下拒绝新的VST前提条件。

做到了什么

该分支作为 PR 30 完成了编译与合并工作。主定理于 4 月 29 日被接受，后续审核则删除了一个过时的“无后向边缘”前提。这仅是一个单独案例，并非控制研究。

上手要点

预计需要严格监管：十天内约59小时使用Codex，415个人类提示词，13,305次工具调用，未观察到速度提升。