AI-Assisted Completion of CertiGC Proofs: An Experience Report

Shengyi Wang

This experience report describes the Codex-assisted completion and stabilization of a substantial Rocq (formerly Coq) proof development for CertiGC, the verified generational garba…