Curriculum proof repair with learned counterexamples

Formal verification provides strong correctness guarantees, but proof development remains difficult because developers must diagnose coarse verifier errors and repair failed proof obligations. Recent approaches leverage language models (LMs) to improve proof automation through verifier-in-the-loop repair, but they often rely on hand-engineered prompts, retrieved examples, or sparse pass/fail feedback. We present \tool, an LM-based framework for Verus proof repair that internalizes counterexample-guided diagnosis as a model capability. Our key insight is to train counterexample generation not as a standalone validation task, but as a data-driven diagnostic objective: a counterexample is useful when conditioning on it helps the model produce a safe, verifier-passing proof. Given a failed Verus proof and verifier error, \tool generates a structured source-level counterexample, repair rationale, and repaired proof in one trajectory, optimized with reinforcement learning from Verus feedback and a proof-code safety gate. To address sparse and order-sensitive credit assignment, \tool introduces a topological graph reward that derives invariant dependencies from inductiveness tests and encourages counterexample generation following the same topological order as the invariant dependencies. Across seven Verus benchmarks with 471 problems, \tool achieves 61.6\%/72.2\% weighted-average Safe-Pass@1/Safe-Pass@3, outperforming the strongest baseline, Claude Sonnet 4.5, by 5.7/6.3 points. We also show that \tool's learned counterexample can directly augment the reasoning of existing LM-based proof repair approaches, improving their success rate by 64.3\% compared to using the chain-of-thought diagnostics.