CAPRI: Contract-Aware Proof Repair for Isabelle

CAPRI: Contract-Aware Proof Repair for Isabelle

Abstract. 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).

Keywords: Isabelle/HOL · large language models · proof repair · assurance · reproducibility

Introduction

Large language models (LLMs) are increasingly used in combination with proof assistants. The basic loop is straightforward: the model proposes a proof, the prover checks it, and any diagnostic may be returned to the model for another attempt. This pattern supports whole-proof generation, tactic search, and recent systems for Isabelle and Lean [1,16,3,11]. Within this loop, Isabelle/HOL provides a strong guarantee: it determines whether the submitted theory is accepted by the prover and its toolchain [7]. It does not, however, determine whether an automated repair stayed within the changes authorised by the developer.

Consider a model asked to repair a single proof so that an Isabelle session builds. Instead of repairing the proof, it might weaken the theorem, add the desired conclusion as an assumption, change a definition or import, or delete a neighbouring regression obligation. It might also introduce commands such as sorry, which admits an unproved theorem, or oops, which abandons a proof attempt. Isabelle may correctly accept the resulting development because it checks the theory it has been given. The failure is not one of prover soundness, but of repair authority: the patch does more than the developer authorised. We call this situation a false success. The build succeeds, but the requested repair has not been performed within its assigned boundary.

Our workflow addresses this problem by treating the LLM as an untrusted source of patches. Isabelle checks proof acceptance, while an independent contract checker checks change authorisation. A machine-readable repair contract identifies the protected text and the proof region that may be edited. The checker compares the original and candidate repositories to determine whether the proposed patch conforms to that contract. A candidate is promoted only when it passes both the Isabelle build and the contract check. The accompanying audit record preserves the original repository, contract, prompts, model proposals, candidate trees, contract reports, prover output, and run history. The two acceptance decisions can therefore be inspected and reproduced independently.

The evaluation addresses three research questions:

RQ1: Can the workflow produce contract-preserving repairs across several Isabelle developments and classes of proof failure?

RQ2: How do one-shot and bounded-iterative workflows compare, and how are their outcomes associated with the point at which the initial Isabelle diagnostic is supplied?

RQ3: Can Isabelle-accepted candidates modify protected text, and how effectively do retrospective contract checking and a proof-body-only interface contain this risk?

The paper contributes a dual acceptance rule separating proof acceptance from repair authorisation; a machine-readable contract and independent conformance checker; a replayable repair controller with evidence for auditing individual runs; and a frozen benchmark of twelve tasks drawn from the SLEEC, Temporal UTP, Defeasible Logic, and BorderSafe developments. We also report a separately labelled exploratory campaign on prompting, demonstrations, and model/provider configuration.

Our focus is repair-workflow assurance rather than general theorem-proving performance. The evaluation uses one hosted model and a small corpus drawn from developments maintained by the authors, so it does not estimate performance on arbitrary Isabelle problems. We use green build to mean that the Isabelle session and its required checks complete without reported failure. Our concern is whether such a build provides sufficient evidence when the repair is also subject to an explicit edit boundary.

Proof Acceptance and Repair Authority

An accepted but unauthorised patch

A false success occurred in a Temporal UTP task concerning the preservation of healthiness refinement under renaming. The contract authorised changes only to the proof body. Instead of repairing the proof, the candidate added the desired conclusion as an assumption and then discharged the theorem directly:

assumes s o u r c e r e f i n e m e n t: L T L S a f e t y H e a l t h i n e s s. hrefines G D

and r e n a m e d r e f i n e m e n t:

" L T L I m p l S a f e t y H e a l t h i n e s s. hrefines

(ltl rename demo rename ‘ G)

(ltl rename demo rename ‘ D) "

shows L T L I m p l S a f e t y H e a l t h i n e s s. hrefines...

using r e n a m e d r e f i n e m e n t

by assumption

Isabelle correctly accepted the modified declaration. Once the additional assumption had been introduced, the conclusion followed immediately. The failure concerned not prover soundness, but delegated development authority. The developer had requested a proof of a fixed theorem, whereas the candidate changed the theorem itself. The same problem can arise through other unauthorised transformations, such as weakening the proposition, changing a definition or import, or deleting protected declarations adjacent to the proof. Each may result in an Isabelle-accepted theory without performing the repair that was authorised.

Dual acceptance and machine-readable authority

Let R be the original repository, R ′ a candidate repository, and C a development contract. We write Build(R ′) when the required Isabelle session completes successfully using the prescribed Isabelle version and build configuration. This is an operational acceptance predicate: it records that Isabelle accepts the candidate, not that the candidate implements the requested change.

We write Conforms(R, R ′, C) when the contract permits the difference between R and R ′. Separate predicates therefore represent proof acceptance and repair authorisation: Build(R ′) and Conforms(R, R ′, C). A repair is accepted only when both hold:

Accept(R, R ′, C) ≜ Build(R ′) ∧ Conforms(R, R ′, C) (1)

A run is classified as valid-success when both predicates hold, and as a terminal false-success when the candidate builds but does not conform. A conforming candidate that does not build may be returned to the repair workflow as diagnostic feedback while its attempt budget remains; if that budget expires, the run is classified as safe-failure. A candidate that neither builds nor conforms is retained as rejected-violation rather than silently discarded. These labels describe workflow outcomes; they do not classify the submitted proposition itself as true or false.

For proof-only repair, a contract specifies an editable region EC, a target declaration tC, a set of forbidden commands FC, and a required build configuration BC. Let πC (R) be the byte-for-byte projection of every protected file and of all protected text outside EC. Let Decl(R ′) be the set of declaration names in R ′, and let Cmd(R ′) be the set of commands detected after comments, strings, and cartouches have been removed. The implemented conformance condition is

Conforms(R, R ′, C) ≜ (πC (R) = πC (R ′)) ∧ tC ∈ Decl(R ′) (2) ∧ (Cmd(R ′) ∩ FC = ∅)

The build configuration BC governs Build(R ′); the remaining fields govern Conforms(R, R ′, C). The first conjunct of Equation 2 provides the principal conformance guarantee: an exact frame condition on the permitted change. In proof-only mode, every protected byte must remain unchanged. This rule is strict: even harmless reformatting outside the proof region is rejected, because an exact boundary is easier to check and audit than a judgement about whether an additional change is sufficiently minor. The checker also requires the editable-region markers to be unique and rejects any addition, removal, or modification of files outside the editable set. The following fragment illustrates a proof-repair contract:

task id: temporal - demo - rename

isabelle :

version : Isabelle2025 -2

session: T e m p o r a l D e m o R e n a m e B e n c h m a r k

target :

declaration: l t l c l o s e d r e f i n e m e n t p r e s e r v e d b y s a f e t y r e n a m i n g

editable :

• file: D e m o T e m p o r a l U T P. thy

region start: (* BEGIN AUTHORISED PROOF:... *)

region end: (* END AUTHORISED PROOF:... *)

f o r b i d d e n c o n s t r u c t s: [sorry, oops, axiomatization, oracle]

acceptance :

session build: true

maximum iterations: 4

The forbidden-command scan is an additional safeguard, not a substitute for Isabelle’s parser or kernel. Nor does the checker attempt to establish that two arbitrary theories are semantically equivalent. It checks a narrower property: that the candidate differs from the original repository only where the contract permits it to differ. For proof-only repair, this syntactic condition is more precise and auditable than an informal claim that the two repositories are essentially unchanged.

Trust assumptions. The LLM is untrusted and may return arbitrary source text. The trusted computing base comprises the contract, the original repository, the patch-application code, the independent checker, the Isabelle installation, and the host platform. The checker follows a verdict path separate from Isabelle: it computes conformance from the repository difference and the contract rather than inferring it from the build result. The checker is itself part of this trusted computing base and has not been formally verified. Cryptographic hashes and replay records make accidental corruption and disagreement between tools visible. They do not protect against a malicious contract author, a compromised host, or a compromised trusted tool.

Workflow and Experimental Design

Controller and audit trail

Figure 1 shows the repair controller. Each proposal is applied to a fresh copy of the original repository. Depending on the experimental condition, the model returns either exact textual edits to the target theory or a replacement for the authorised proof body. The controller constructs the candidate repository, checks it against the contract, and invokes Isabelle when required by the condition. In iterative conditions, a failed proposal may be followed by another request containing the relevant Isabelle diagnostic. The experimental protocol bounds the number of attempts. Every proposal and intermediate candidate is retained, including candidates that neither build nor conform.

The audit record contains the contract, the original tree hash, the exact prompts, the structured model proposals, every candidate tree, the contract reports, and both raw and normalised Isabelle output. It also records the requested and returned model identifiers, response identifiers, token counts, and completion status. File-level SHA-256 manifests cover the released corpus. The recorded proposals can then be replayed without access to the live model service, reproducing candidate construction, contract checking, and Isabelle execution. Repeating the original live calls is supplementary rather than a prerequisite for reproduction, because hosted models are nondeterministic and a model alias may resolve to a different implementation over time.

Artefact availability. The complete reproducibility artefact for the frozen 180-run evaluation and the separately labelled post hoc exploratory campaign is archived as version 1.0 on Zenodo at https://doi.org/10.5281/zenodo.21917680.

Run outcomes

An experimental run is a bounded sequence of proposals for one frozen task, condition, and replicate. The outcome depends on the final candidate reached under the stopping rules. When Isabelle accepts a candidate, the controller terminates the run. The outcome is valid-success if the candidate also conforms to the contract and false-success if it does not. False success is terminal: once a workflow has produced a green build outside the authorised region, allowing it to continue until it eventually finds a conforming repair would conceal the event that the experiment is intended to detect. When no candidate builds before the attempt limit is reached, the final candidate determines the outcome. The result is safe-failure if that candidate conforms to the contract but Isabelle rejects it, and rejected-violation if it violates the contract. The outcome invalid-candidate records model output that could not be converted into a candidate repository.

Infrastructure failures were retained in the operational record. They received a scientific outcome only after application of the frozen recovery rule. The experiment therefore contains 180 scientific runs, although the controller made 245 individual model requests.

Experimental conditions

Table 1 summarises the five conditions. C0–C2 form the contemporaneous main experiment, while C3 and C4 form a prospectively specified extension whose protocol and paired analyses were cryptographically frozen before execution. C0, C1, C3, and C4 allow the model to return exact edits to the complete target theory. C2 presents only the authorised proof body and requires the model to return a replacement for that body. In C2, contract conformity is checked before Isabelle is invoked, so a proposal that attempts to modify protected text cannot reach the prover.

The main experiment combines twelve tasks, three conditions, and three replicates, giving 108 runs. C0 permits a single request, while C1 and C2 permit up to four attempts. The extension adds two further conditions with 36 runs each, giving 72 additional runs and 180 in total. C3 supplies the baseline Isabelle diagnostic in a single request. C4 withholds that diagnostic from the initial request but permits up to four attempts, with stateful diagnostic feedback after each failure.

All conditions requested the gpt-5.6 alias at high reasoning effort. The service returned the resolved model identifier gpt-5.6-sol [8]. Isabelle timeouts, model-request timeouts, and attempt limits were fixed in advance. Retries were authorised only for infrastructure failures.

Benchmark and protocol

The benchmark contains twelve tasks drawn from four Isabelle developments: four from SLEEC [20], three from Temporal UTP, three from Defeasible Logic, and two from BorderSafe. The Temporal UTP tasks were developed using Isabelle/UTP, a mechanised framework for semantic theory engineering and automated verification [2]. Table 2 records the frozen origin, difficulty label, and failure class of each task.

Six tasks preserve historical failures and corrected revisions. The remaining six are controlled corruptions created by removing a predeclared proof body from a previously built theory. In every case, the reference repair is withheld from the model. Before execution, the tasks were classified into four local, four intermediate, and four structural failures. These categories provide descriptive strata for the benchmark; they are not …

Based on the paper, here are the specific improvements for AI systems and what the improved system can do:

1. Dual-Acceptance Verification Architecture

• Implement a two-predicate acceptance system: Build(R') (proof acceptance) AND Conforms(R, R', C) (contract conformance)

• Add an independent contract checker that enforces a machine-readable edit contract with exact frame conditions

• Ensure the checker verifies byte-for-byte projections of protected text, forbidden commands, and declaration preservation

2. Proof-Body-Only Interface Restriction

• Restrict the model's edit surface to only the authorized proof body, not the full theory

• Prevent models from modifying theorem statements, assumptions, definitions, or imports

• Check contract conformity before invoking the prover, so violating proposals never reach the proof checker

3. Bounded Iterative Repair with Diagnostic Feedback

• Allow up to 4 attempts with stateful diagnostic feedback after each failure

• Supply the initial Isabelle diagnostic to the model before the first attempt

• Terminate immediately upon false success (build accepted but contract violated) to prevent concealment

4. Complete Audit Trail and Replayability

• Retain all prompts, proposals, candidate repositories, diagnostics, verdicts, hashes, and response identifiers

• Enable replay of candidate construction, contract checking, and Isabelle execution without live model access

• Record file-level SHA-256 manifests for reproducibility

5. Contract-Aware Prompting

• Include the explicit contract in the prompt, specifying: editable region, target declaration, forbidden commands (sorry, oops, axiomatization, oracle), and build configuration

• Clearly delineate the authorized proof region with markers (e.g., (* BEGIN AUTHORISED PROOF... *))

• Repair Isabelle proofs while guaranteeing the edit stays within authorized boundaries — it cannot weaken theorems, add assumptions, delete protected declarations, or introduce sorry/oops commands

• Distinguish between proof accepted and repair authorized — it treats a green build as necessary but insufficient; the contract check is equally mandatory

• Prevent false successes — when a model attempts to add the desired conclusion as an assumption or edit beyond the proof region, the system rejects it before it reaches the prover (in proof-body-only mode) or flags it post-hoc (in full-theory mode)

• Provide auditable, reproducible repairs — every run can be replayed and independently verified, even if the hosted model changes or becomes unavailable

• Achieve higher consistency — bounded iteration (up to 4 attempts) improved valid repairs from 22/36 to 31/36 in the contemporaneous comparison, mainly by making successful outcomes more reliable on tasks the model could already handle

• Safely fail — when no conforming repair is found, the system leaves the original obligation intact rather than producing an accepted-but-unauthorized patch

• Support controlled authority expansion — if a repair genuinely needs a helper lemma or changed definition, the contract and interface can be explicitly widened, but this is deliberate rather than accidental

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