修证明怕改掉命题？核对假设再提小修补
在 Codex 提供Rocq 测试项目与证明义务，按下方测试流程制作最小证明修补与检查记录，再由人核对；须另备匹配工具与权限。
执行环境与使用方式
AI／软件
Codex
在哪里操作
电脑终端中的 Codex CLI；在独立测试文件夹打开。
如何开始
- 按来源中的官方安装指南设置 Codex CLI；在测试文件夹打开终端，输入 codex 并登录。
- 只提供Rocq 测试项目与证明义务与下方提示词；先确认范围，再允许必要操作。
- 核对实际产出的最小证明修补与检查记录；记录未执行或无法验证的部分。
准备与方案条件
需要 Codex 使用权、获准的测试数据及匹配的运行环境；写文件与终端命令须在允许范围内。具体准备：需要熟悉形式验证的审查者、可重建的证明专案及版本固定的测试分支。 需固定版本的 Rocq 与项目依赖包，并由熟悉形式证明的人审核；普通聊天无法代替证明内核检查。
提示词移植限制
文字要求可改给其他代码助手；但文件权限、运行环境、测试工具及集成须另行设置，不能只换工具名称就视为兼容。
使用限制
本流程未实测；只在测试副本内工作，不自动发布、付款或改正式数据。将规划、实际操作结果与未测项目分开。
环境资料来源
- https://developers.openai.com/codex/cli/ · 2026-10-19
適用情境 / When to use
在 Codex 提供Rocq 测试项目与证明义务，按下方测试流程制作最小证明修补与检查记录，再由人核对；须另备匹配工具与权限。 Shengyi Wang 报告用 Codex 协助完成与稳定 CertiGC 的 Rocq 证明。
步驟 / Steps
- 需要熟悉形式验证的审查者、可重建的证明专案及版本固定的测试分支。
- 选定未完成的证明义务，要求说明依赖的定义与假设后再提出修补。
- 重新执行证明核心，逐行比较定理、前提与公理，避免把目标偷偷改弱。
提示詞 / Prompt
在［证明专案测试分支］处理［指定证明义务］，保持［定理及允许假设］不变。先列依赖，提出最小修补并提供核心检查纪录；若需更动规格或增加公理，停止并解释。输出差异供专家审查。
留意事項 / Cautions
- 不得把新增公理或跳过证明当作完成。
- 不应由此宣称整个系统安全或适合部署。
來源限制 / Evidence limits
经验报告不是对照实验；核心接受证明不等于规格符合现实需求。
流程說明 / Workflow note
以下步骤与提示词为本站原创、未实测的练习设计，并非原作者逐字流程；来源结果不代表练习保证成功。
原始工具組合 / Original tool stack
Codex；Rocq／Coq；CertiGC；VST／CertiGraph
来源发表日期：2026-06-19
来源查核日期：2026-10-19
AI-Assisted Completion of CertiGC Proofs: An Experience Report