AI-Assisted Completion of CertiGC Proofs: An Experience Report

Technical Summary: AI-Assisted Completion of CertiGC Proofs

Problem Statement
This experience report addresses the challenge of extending a verified generational garbage collector (CertiGC) from an effectively immutable setting to a mutable one within the CertiGraph project. The original CertiGC proof relied on a global no_backward_edge invariant, which assumed that older objects could not acquire pointers to younger objects. This assumption holds for immutable data but is invalidated by mutable updates (e.g., ML-style references or lazy thunk updates), where a write barrier may create pointers from older to younger generations.

The core technical problem was not merely scripting new proofs, but repairing the verification architecture. The old invariant was semantically false for the new code, meaning the existing proof path could not simply be patched; the specification and the mathematical theorems had to be reorganized. The goal was to re-establish the top-level graph-isomorphism correctness theorem while accommodating mutable updates, without weakening the theorem's statement or introducing incorrect preconditions.

Methodology
The authors utilized OpenAI Codex as an agentic coding tool to assist in repairing and stabilizing the proof development. The workflow was characterized as supervised, checker-driven proof maintenance rather than autonomous proof generation.

1. Workflow Structure:

   • Human Role: The human proof engineer adjudicated invariant proposals, constrained specification changes, reviewed theorem statements, and decided when proof cleanup was justified. The human ensured that the semantic contract of the collector was preserved.
   • AI Role: Codex acted as an agent that read the codebase, edited proof files, executed targeted builds, diagnosed errors, proposed helper lemmas, and performed cleanup.
   • Tooling: The process utilized a locally configured Rocq-MCP (Model Context Protocol) server, allowing Codex to interact directly with the Rocq kernel to inspect proof states, run tactics, and query environments. This reduced the edit-compile-read-error cycle.

2. Repair Strategy:

   • Invariant Replacement: The central technical shift was replacing the invalid no_backward_edge condition with a new recorded-backward-edge invariant (no_unrecorded_backward_edge). This new invariant states that every backward edge (from an older to a younger generation) must be recorded in the appropriate remembered-set component.
   • Proof Architecture: The repair involved three main phases:
     1. Repairing the Verified Software Toolchain (VST) proofs for do_generation to incorporate the forward_remset function and expose the correct abstract relation.
     2. Restoring the outer garbage_collect VST proof to preserve remembered-set invariants across collection and reset.
     3. Re-establishing the mathematical gc_correct.v theorem, proving that the abstract collection relation preserves roots-level graph isomorphism.
   • Post-Theorem Audit: Crucially, the work did not end when the main theorem was accepted. A subsequent audit removed the stale no_backward_edge condition from the VST-facing specification path, ensuring the final artifact matched the mutable collector's semantics.

Key Contributions

• Invariant Repair Case Study: The paper documents a specific instance where the primary challenge was replacing a semantic assumption invalidated by code changes (mutation) rather than adapting a nearby proof architecture.
• Division of Labor: It delineates a concrete workflow where the AI proposes invariants and implements preservation lemmas, while the human engineer validates the semantic correctness of these proposals and guards against specification drift (e.g., preventing the leakage of internal collector state into the public theorem).
• Interaction Statistics: The report provides transcript-derived statistics (415 human prompts, 13,305 tool calls, ~59.3 active AI hours) to characterize the nature of the collaboration as sustained, iterative, and heavily dependent on machine-checking feedback.
• Artifact Stabilization: The resulting proof artifact successfully merges the mutable collector logic into the mature CertiGraph/VST codebase, maintaining the graph-isomorphism theorem over ordinary program roots.

Results

• Successful Integration: The repaired branch was merged into the upstream CertiGraph repository (Pull Request 30, commit 85da48e4) on May 3, 2026.
• Proof Acceptance: The Rocq kernel accepted the main theorem garbage_collect_isomorphism on April 29, 2026.
• Artifact Quality: The final proof artifact touched 18 files, with significant changes in GCGraph.v (invariant library) and gc_correct.v (mathematical theorem). The VST proofs in verif_do_generation.v and verif_garbage_collect.v were successfully repaired to reflect the new forward_remset call sequence.
• Semantic Correction: The audit phase successfully identified and removed the obsolete no_backward_edge premise from the specification boundary, ensuring the theorem's assumptions were justified by the actual mutable collector semantics.

Significance and Claims
The paper modestly claims that agentic assistants can materially assist in checker-driven proof repair for large, mature formal developments, provided that candidate invariants and specification changes are continuously reviewed by a human.

• Not Autonomous Discovery: The authors explicitly state they do not claim autonomous proof discovery. The AI did not independently discover the entire architecture; the human engineer was essential in recognizing that the old invariant was invalid and in accepting the new recorded-backward-edge invariant as the correct semantic replacement.
• Maintenance vs. Adaptation: Unlike previous reports where AI adapted existing proof architectures (e.g., CertiCoq's ANF transformation), this work demonstrates AI's utility in invariant repair within a systems-verification context where the core assumptions of the existing architecture were broken.
• The Role of the Human: The human's role shifted from writing proof scripts to adjudicating the "truth" of the specification. The paper argues that while AI can handle the mechanical propagation of invariants and local script repair, the critical decision of "what should be true" (the semantic contract) remains a human responsibility.
• Tooling Implications: The experience suggests that proof-assistant support for agentic tools should evolve to expose not just errors, but also obligation structures and dependency information to make repair less dependent on repeated shell builds.

In conclusion, the paper presents a pragmatic mode of AI-assisted formal proof development where the AI acts as a persistent collaborator for local repair and invariant propagation, while the human engineer maintains the guardrails of semantic correctness and theorem integrity.