Zoe Paraskevopoulou

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)

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 administrati...