AI 보조를 통한 CertiGC 증명 완성: 경험 보고서

이 경험 보고서는 CertiGraph 프로젝트의 검증된 세대별 가비지 컬렉터(generational garbage collector)인 CertiGC를 위해, Codex의 보조를 받아 대규모 Rocq (이전의 Coq) 증명 개발을 완성하고 안정화한 과정을 기술합니다. 이 개발은 수집 경로(collection path)에 remembered-set 포워딩을 추가하고 최상위 그래프 동형성(graph-isomorphism) 정확성 정리를 재정립함으로써, 컬렉터를 사실상 불변(effectively immutable)인 환경에서 가변(mutable) 환경으로 확장합니다. 핵심적인 기술적 문제는 단순히 저수준의 증명 스크립팅(proof scripting)만이 아니었습니다. 가변 업데이트는 기존의 전역적인 'no-backward-edge' 가정을 무효화하므로, 모든 역방향 엣지(backward edge)가 적절한 remembered-set 구성 요소에 기록된다는 'recorded-backward-edge' 불변량(invariant)을 중심으로 증명을 재구성해야 했습니다. 이 사례는 최근의 AI 보조 형식 증명(formal-proof) 사례들과는 다릅니다. 인접한 컴파일러 증명 아키텍처를 조정하거나 새로운 메타이론(metatheory)을 형식화하는 것과 달리, 본 사례는 Rocq로 기계화된 Verified Software Toolchain (VST) 및 CertiGraph를 기반으로 구축된 성숙한 코드베이스에서 장기간 진행되어 온 검증 작업을 완성하는 것입니다. Rocq 커널은 정확성의 중재자 역할을 유지했으며, 우리의 역할은 불변량 제안을 판결하고, 사양(specification) 변경을 제한하며, 정리(theorem) 문구를 검토하고, 증명 정리(proof cleanup)가 정당화되는 시점을 결정하는 방향으로 전환되었습니다. Codex 보조 단계에서는 먼저 VST 관계 증명을 수리한 다음, 수학적 그래프 동형성 정리를 복구하였고, 그 후에야 VST 사양에서 정리로 이어지는 전제 경로(premise path)를 감사(audit)했습니다. 이 감사 과정에서 VST를 향하는 증명 경로로부터 오래된 no-backward-edge 조건을 발견하여 제거했습니다. 본 보고서는 워크플로우, 결과물로서의 증명 아티팩트(proof artifact), 그리고 에이전트 기반 증명 유지보수(agentic proof maintenance)를 위한 교훈을 제시합니다.