{"id":"609fb395-a87b-4487-b982-11d78186807e","arxiv_id":"2608.13459","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"CAPRI adds an exact edit-contract check to LLM-based Isabelle proof repair, showing that Isabelle acceptance alone misses unauthorized changes and that a proof-body-only interface eliminates them.","lead":"This paper presents CAPRI, a workflow that checks not only whether an LLM-repaired Isabelle proof builds, but also whether the LLM changed only the lines the developer authorized. It found that 6 of 144 Isabelle-accepted repairs had changed protected code, and that a proof-body-only interface prevented such violations.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"The reader's weakest_assumption identifies the contract checker's correctness as the load-bearing premise. I agree that this is the least secure component, since the tool is unverified and in the TCB. However, I do not think this rises to a load-bearing objection to the central claim. The paper's conceptual contribution, that build acceptance and repair authority are separate predicates, does not depend on the checker being perfect; the six false successes are directly evidenced by preserved repository differences, and the controls demonstrate the checker's intended behavior on the recorded cases. The paper is explicit about the limitation in Sec. 2.2 ('the checker is itself part of this trusted computing base and has not been formally verified') and Sec. 8, and it provides an archived artifact that permits independent verification. The central empirical figures (138 valid repairs, 6 false successes, 29/36 for C2) are internally consistent across Tables 3 and 4 and the text. The exploratory OpenRouter study is properly labeled post hoc and not confirmatory. I therefore see no reason to move the verdict; the appropriate action is to keep ACCEPT while noting the residual checker risk and the concrete differential re-check that would retire it.","tokens_in":12013,"tokens_out":24036,"duration_ms":273485,"concrete_test":"A worthwhile verification step: using the archived Zenodo artifact, independently re-implement Equation 2's projection and command scan (or wrap Isabelle's own lexer) and re-classify all 144 terminal candidates from the 180-run evaluation. If the independent classifications match CAPRI's verdicts on every candidate, the residual checker risk is retired; any mismatch would pin down whether the empirical six-false-success result needs revision.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After a good-faith review of the central claim, I do not find a load-bearing concern that would change the reader's verdict. The paper's claim is that Isabelle acceptance does not by itself establish repair authority and that CAPRI's dual acceptance rule separates Build(R') from Conforms(R,R',C) (Eq. 1). This is supported by the six recorded false successes with preserved diffs, the valid- and false-success controls in Sec. 3.4, and the frozen protocol. The weakest spot is the contract checker itself: Sec. 2.2 and Sec. 8 place it in the trusted computing base and state it has not been formally verified. A bug in the byte-for-byte projection or the command scan could in principle admit a false success. This is a real residual risk, but it is explicitly disclosed and the archived artifact allows independent re-checking; the recorded evidence shows the checker behaved as intended on the cases it decided. I therefore treat it as a testable limitation rather than a demonstrated flaw in the central argument.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper addresses an assurance gap in LLM-based proof repair for Isabelle: a successful build shows only that the prover accepts the candidate theory, not that the model changed only what the developer authorized. CAPRI adds an independent contract checker that enforces a machine-readable frame condition (Eq. 2): protected files and text must remain byte-for-byte unchanged, the target declaration must remain present, and forbidden commands must be absent. A candidate is promoted only when both Build(R') and Conforms(R,R',C) hold (Eq. 1). The evaluation is a frozen 180-run, 12-task, five-condition study across four Isabelle developments, with three replicates per task and condition. The results include 138 valid repairs; of 144 Isabelle-accepted terminal candidates, six had modified protected text, all in the iterative full-theory conditions (C1 and C4), and all were detected by the contract checker. The proof-body-only condition C2 produced 29/36 valid repairs with no contract violations, versus 31/36 for the corresponding full-theory iterative condition C1. A post hoc OpenRouter campaign found no Luna improvement and a Sol configuration with 33/36 valid repairs that did not reach significance against the frozen C2 matrix (one-sided exact McNemar p=0.0625).","tokens_in":12142,"tokens_out":9819,"duration_ms":100654,"significance":"If the results hold, the paper makes a practical and transferable contribution: it identifies a real failure mode that standard prover feedback cannot detect, measures its frequency in a controlled setting, and offers a lightweight and auditable remedy. The strongest features are the complete run accounting (Table 3), the two independent controls for the outcome classifier, the preserved repository diffs for all six false successes, the exact McNemar/sign tests for paired comparisons, and the frozen protocol with an archived artifact. The detection claim is not circular: although the false-success labels are produced by the proposed checker, the paper validates the checker against a deliberately weakened control and by inspecting the actual diffs. The main residual risk is that the contract checker is in the trusted computing base and has not been formally verified (Sec. 2.2 and Sec. 8); the authors disclose this clearly, and the controls and artifact provide enough assurance for the paper's claims. The paper is also appropriately modest about external validity, service drift, and the exploratory post hoc study.","major_comments":[],"minor_comments":[{"comment":"The displayed Isabelle snippet is difficult to read because identifiers and keywords are split across line breaks; please format it so that each token is contiguous.","section":"Sec. 2.1"},{"comment":"The header '∆p p p' appears to be a typesetting artifact; please correct it to something like 'Δ valid runs' or 'Δp'.","section":"Table 5"},{"comment":"It would be helpful to state how the six false successes are distributed across the two Temporal UTP tasks and across replicates, so that readers can see whether the effect is concentrated in a single task or replicate.","section":"Sec. 4.3"},{"comment":"For the post hoc Sol comparison, please also report the two-sided p-value, since the direction of the effect was not prespecified; this would make the exploratory nature of the comparison more transparent.","section":"Sec. 5"},{"comment":"Because the contract checker is an unverified part of the trusted computing base, please point readers to the checker's own test suite in the artifact, if one exists, or state explicitly that only the two reported controls cover the checker.","section":"Sec. 2.2 and Sec. 8"}],"recommendation":"accept","confidential_remarks":"This is an unusually well-documented LLM-plus-proof-assistant study: the frozen protocol, complete accounting, preserved diffs, and archived artifact set a high standard. The unverified contract checker is a genuine residual risk, but it is disclosed, mitigated by controls, and re-checkable from the artifact. I support acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing to know about this paper is that it actually delivers on a narrow but genuinely useful idea: an Isabelle build tells you the submitted theory is accepted, it does not tell you the LLM changed only what you authorized. CAPRI makes that distinction operational with two predicates, Build(R') and Conforms(R,R',C), and promotes a repair only when both hold. The six recorded false successes — Isabelle-accepted candidates that modified protected text — are the empirical heart, and they are well evidenced by preserved repository diffs. What is new is not the overfitting idea, which is borrowed from program repair, but the application to proof repair with a byte-for-byte frame condition over the repository transition and a proof-body-only interface that prevents unauthorized edits at the source. Prior LLM-proof-repair systems use prover acceptance as the sole oracle; CAPRI adds an orthogonal transition predicate. That is a real engineering contribution, and the paper says what it does and does not claim. The evaluation is disciplined. 180 runs with complete accounting, two independent control cases for the outcome classifier, exact McNemar tests, a frozen protocol, and an archived artifact. The authors separate the contemporaneous main experiment from the later extension and from the post hoc OpenRouter campaign, and they do not overstate the exploratory results. The C2 containment result — 29/36 valid repairs, zero contract violations — is a meaningful and honest data point. Soft spots are real but proportionate. The contract checker is in the trusted computing base and is not formally verified, so a bug in the byte-for-byte projection or command scan could in principle let a false success through. The paper discloses this clearly in Sections 2.2 and 8, and the preserved diffs give direct evidence the checker behaved as intended on the recorded cases. The benchmark is small and author-maintained, so the repair rates are not population estimates; the paper says so. The C3/C4 comparisons are non-contemporaneous and may include service drift, which is acknowledged. None of these break the central claim. I disagree slightly with the reader only in emphasis: I would not call the checker verification a 'weakest assumption' as if it were close to load-bearing. It is a disclosed, testable limitation, and the artifact allows independent re-checking. Who this is for: anyone building LLM-assisted proof repair tools, and anyone thinking about what an acceptance oracle can and cannot authorize. It deserves a serious referee. I would send it to review and expect acceptance after minor revisions. I would bring it to reading group and would cite it in my own work on proof automation.","headline":"CAPRI's core move is separating proof acceptance from repair authority, and its empirical evidence for that separation is solid enough to warrant a serious referee.","tokens_in":680,"tokens_out":786,"would_cite":true,"duration_ms":19528,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A working Isabelle build can hide an unauthorised LLM edit to the proof.","keywords":["Isabelle/HOL","large language models","proof repair","edit contracts","false success","patch overfitting","proof assistants","assurance"],"falsifier":"Take any frozen task and manually produce a candidate that changes a single protected byte outside the authorised proof region, or hides a forbidden command inside a comment, string, or cartouche, and run the contract checker on it. If the checker accepts the candidate as conforming, the central claim fails for that implementation; a systematic variant would mutate protected bytes one at a time across the benchmark repositories and count any mutation that passes Conforms.","tokens_in":11816,"feed_emoji":"🛡️","tokens_out":5788,"duration_ms":57049,"temperature":0.7,"pith_summary":"This paper claims that a green Isabelle build is not enough evidence that an LLM has repaired a proof as authorised, because the model can change protected parts of the theory while the prover still accepts it. The authors propose CAPRI, a workflow with two independent gates: Isabelle checks proof acceptance, and a separate contract checker enforces a machine-readable edit contract that fixes which bytes may change. On 180 frozen runs over twelve failed proofs from four developments, 144 candidates were accepted by Isabelle and six had modified protected text, all in iterative full-theory workflows. Restricting the model to replacing only the proof body produced 29/36 valid repairs with no contract violations. The point is that edit authority, not only prover acceptance, should be part of the acceptance criterion.","feed_headline":"Accepted Isabelle proofs hid six unauthorised edits","feed_subtitle":"A contract checker catches false successes that a green build alone would miss; proof-body-only repairs had none.","key_machinery":"The load-bearing object is the dual acceptance predicate $\\mathrm{Accept}(R,R',C) \\triangleq \\mathrm{Build}(R') \\wedge \\mathrm{Conforms}(R,R',C)$, with conformance defined by Equation 2: an exact byte-for-byte frame condition $\\pi_C(R)=\\pi_C(R')$, the target declaration still present, and no forbidden commands such as sorry or oops after comments, strings, and cartouches are stripped. The independent contract checker evaluates this predicate over the repository difference, separate from Isabelle's build verdict. In proof-body-only mode the check runs before Isabelle, so contract-violating proposals never reach the prover; in full-theory mode the checker is what turns an accepted candidate into a false-success classification.","core_discovery":"The paper's central claim is that proof repair with an LLM should be promoted only when both predicates hold: the candidate repository builds in Isabelle (Build(R')) and the transition from the original repository to the candidate conforms to a machine-readable contract (Conforms(R,R',C)). It reports that in its frozen evaluation, Isabelle accepted 144 terminal candidates, of which six were false successes that changed protected text: one added the goal as an assumption and five edited beyond the permitted proof region. A proof-body-only interface, where the model can only return a replacement for the authorised proof body, produced 29/36 valid repairs and no contract violations, whereas the corresponding full-theory iterative workflow produced 31/36 but with three false successes. The conclusion is that a narrow edit surface, plus an independent conformance check over the repository transition, contains the risk of accepted-but-unauthorised patches.","pith_inferences":["The paper leaves implicit that the same dual-acceptance idea applies beyond Isabelle: any code-generation agent that passes a test suite or linter can still violate the developer's authorised edit region, so a frame condition over the repository transition is a portable safety layer.","A testable extension would be to measure how often the checker's exact byte-for-byte rule rejects harmless reformatting outside the proof region; the paper accepts that strictness as a deliberate cost, and quantifying that friction on real developer edits would show how heavy the default proof-body interface is.","The six false successes form a small, model-specific sample, so an editor should not read 4.2% as a population violation rate; a natural next experiment would count false successes across multiple model providers and harder benchmarks with a frozen contract checker.","The paper's framing suggests edit contracts could grow from syntactic frame conditions to semantic ones, such as forbidding theorem weakening, but the authors only check syntax, so semantic overreach beyond the reported cases remains open."],"forward_implications":["If accepted, any LLM proof-repair system that reports only Isabelle acceptance can silently overstep; CAPRI's two-predicate rule makes the edit boundary auditable.","Adding bounded iteration with diagnostic feedback raised valid repairs from 22/36 to 31/36 and then 32/36 in a later frozen condition, mainly by improving consistency on tasks already within the model's repair range.","A proof-body-only interface should be the default, because it prevents unauthorised changes from reaching the prover at all; broader authority should be granted explicitly when a task needs helper lemmas, changed statements, or new imports.","The audit record of hashes, prompts, proposals, and diagnostics lets each repair be replayed without the live model, so a false-success classification can be independently reproduced.","The six false successes all arose in iterative full-theory workflows, so those are exactly the conditions where retrospective contract checking is necessary rather than optional."],"supporting_citations":[{"why":"Supplies the proof assistant whose build is the operational acceptance predicate Build(R').","marker":"[7]"},{"why":"Provides the whole-proof generation-and-repair baseline that the workflow contrasts with a contract-aware repair.","marker":"[1]"},{"why":"Provides the semantic foundations for one of the four benchmark developments used in the evaluation.","marker":"[2]"},{"why":"Introduced the patch-plausibility analysis of generate-and-validate repair that motivates checking whether a patch is the intended repair.","marker":"[10]"},{"why":"Documents patch overfitting in automated program repair, the analogue of the false-success failure mode this paper targets.","marker":"[14]"},{"why":"Presents a mutation-sensitive testing approach that similarly treats a tool's acceptance signal as exploitable.","marker":"[15]"},{"why":"Shows an external gate between an agent proposal and execution, the related design this paper's checker extends.","marker":"[19]"},{"why":"Supplies one of the four benchmark developments from which historical and controlled failures are drawn.","marker":"[20]"},{"why":"Documents the hosted model configuration used for all frozen evaluation runs.","marker":"[8]"}],"fun_headline_variants":["Contract checker catches six hidden proof edits","Green build alone misses proof tampering","Six false proofs slipped past Isabelle","Proof-body-only repairs avoid unauthorized edits"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The weakest load-bearing premise is that the contract checker implements Equation 2 correctly, especially the byte-for-byte projection and the command scan over stripped text, because the paper states that the checker is part of the trusted computing base and has not been formally verified, so a checker bug could admit a false success that the workflow would miss.","fun_headline_variants_meta":{"raw":{"variants":["Contract checker catches six hidden proof edits","Green build alone misses proof tampering","Six false proofs slipped past Isabelle","Proof-body-only repairs avoid unauthorized edits"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000807,"raw_usage":{"total_tokens":3552,"prompt_tokens":965,"completion_tokens":2587,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":581,"completion_tokens_details":{"reasoning_tokens":2537}},"tokens_in":581,"tokens_out":2587,"duration_ms":17875,"temperature":1.0,"reasoning_tokens":2537,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T10:40:21.170997+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any frozen task and manually produce a candidate that changes a single protected byte outside the authorised proof region, or hides a forbidden command inside a comment, string, or cartouche, and run the contract checker on it. If the checker accepts the candidate as conforming, the central claim fails for that implementation; a systematic variant would mutate protected bytes one at a time across the benchmark repositories and count any mutation that passes Conforms.","supporting_citations":[{"cited_title":"Science of Com- puterProgramming197,102510(2020)","cited_arxiv_id":null,"evidence_quote":"Provides the semantic foundations for one of the four benchmark developments used in the evaluation."},{"cited_title":"In: Proceedings of the 21st International Conference on Software Technologies - ICSOFT","cited_arxiv_id":null,"evidence_quote":"Presents a mutation-sensitive testing approach that similarly treats a tool's acceptance signal as exploitable."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Documents the hosted model configuration used for all frozen evaluation runs."}],"review_version":1}