Reproduce “AI-Assisted Completion of CertiGC Proofs: An Experience Report” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Shengyi Wang
This experience report details an AI-assisted workflow for repairing the CertiGC proof development, extending its verified generational garbage collector to support mutable references. The work demonstrates how an AI assistant, guided by a human, successfully replaced a core invariant and re-established the top-level graph-isomorphism correctness theorem, integrating the updated proof into the CertiGraph repository.
Key insights
- AI agents are effective for mechanical invariant propagation, local proof repair, and codebase cleanup in complex formal verification projects, automating tedious and repetitive tasks.
- Human judgment remains critical for high-level proof engineering decisions, such as the selection of core invariants, defining specification boundaries, and ensuring that the verified properties align with the system's intended semantics.
- A post-theorem premise audit is essential to validate that a machine-checked proof certifies the *intended* property, as demonstrated by the removal of a stale invariant from the VST-facing specification path after proof acceptance.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.