一句话：用 Claude Code 智能体从零机械化 CertiRocq 中 ANF 变换的语义保持证明，产出约 6000 行 Rocq 证明，耗时 94.5 小时。
本文是一篇经验报告，探讨利用智能体编程助手（Claude Code，基于 Claude Opus 4.6）在仅有人的指导下、不编写任何人工证明代码的情况下，从零机械化一个规模可观的 Rocq 正确性证明。该证明针对 Rocq 验证编译器 CertiRocq（原 CertiCoq）中的 administrative normal form（ANF）变换，建立其语义保持性。CertiRocq 中密切相关的 continuation-passing style（CPS）变换此前由人类专家耗时数月证明正确。作者以该 CPS 证明为模板，指示 LLM 将证明技术适配到 ANF 场景，而 ANF 在若干重要技术点上与 CPS 不同。最终 ANF 证明约 6000 行 Rocq 证明（大于 4200 行的 CPS 证明），在 94.5 小时内完成。文章描述了证明技术，并报告了使用 LLM 开发该证明的经验，讨论了该方法的优势与局限及其对验证编译器构建的启示。
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without any human-authored proof code. The proof establishes semantic preservation for the administrative normal form (ANF) transformation in the CertiRocq (formerly CertiCoq) verified compiler for Rocq. The closely related continuation-passing style (CPS) transformation in CertiRocq was previously proved correct by human experts over several months. We use this proof as a template and instruct the LLM to adapt the proof technique to the ANF setting, which differs in important technical ways. The resulting ANF proof comprises approximately 6,000 lines of Rocq proof (larger than the 4,200-line CPS proof) and was developed in 94.5 hours. We describe the proof technique and report on the experience of developing it with an LLM, discussing both the strengths and limitations of the approach and its implications for verified compiler construction.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-20082,
title = {Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)},
author = {Zoe Paraskevopoulou},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828700}
}