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.

@article{paperbot3668,
  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}
}