# CAPRI: Contract-Aware Proof Repair for Isabelle

arXiv: https://arxiv.org/abs/2608.13459 · HTML: https://mlsanity.com/paper/2608.13459/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 25 references that are in the map.
- First posted on arXiv 13 Aug 2026.

## Builds on (most cited first, 16 of 16)

- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents](https://mlsanity.com/paper/2603.20449/) (2026)
- [Automated Patch Assessment for Program Repair at Scale](https://mlsanity.com/paper/1909.13694/) (2019)
- [Proof Repair across Type Equivalences](https://mlsanity.com/paper/2010.00774/) (2020)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents](https://mlsanity.com/paper/2307.03697/) (2023)
- [Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP](https://mlsanity.com/paper/1905.05500/) (2019)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Vibe Coding an LLM-powered Theorem Prover](https://mlsanity.com/paper/2601.04653/) (2026)
- [Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4](https://mlsanity.com/paper/2602.08384/) (2026)
- [TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation](https://mlsanity.com/paper/2606.06133/) (2026)
- [IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus](https://mlsanity.com/paper/2606.18098/) (2026)

## Abstract (arXiv)

We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test (p=0.0625).