CAPRI Adds a Machine-Readable Edit Contract to LLM Isabelle Proof Repair — 6 of 144 Accepted Proofs Had Touched Protected Text

arXiv 2608.13459·medium signalXBlueskyLinkedInCopy link

An Isabelle build establishes that a submitted theory is accepted, not that the LLM changed only what the developer authorised. CAPRI pairs Isabelle's check with an independent checker enforcing a machine-readable edit contract, retaining prompts, proposals, candidate repositories, diagnostics, verdicts and hashes for audit. Across five workflows on twelve failed proofs from four developments (180 runs, 138 valid repairs), six of 144 Isabelle-accepted terminal candidates had modified protected text — all from iterative workflows able to edit a complete theory. A proof-body-only interface produced 29/36 valid repairs with zero contract violations versus 31/36 for the equivalent full-theory workflow, quantifying the small correctness cost of the tighter edit surface.