FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, table row, page reference, quotation and the appendix prompts and counts; changed: the six Table 4 incidents were called wrong earlier measurements of the author and the leak incidents the author’s own runs, which the paper does not say; the leak evidence was widened to similarity alone while the paper also cites transcript and access records; the sentence that no technique has a measured effect ignored the one single-run retrieval comparison; the heading claimed every known way; three unmarked inferences marked; the import wording and a one run wording fixed; not checked: the Verus claims that Verus has no command listing assumptions and no independent proof checker, which the Verus references do not address.

source: Naing Oo Lwin (Astrio Labs), arXiv:2610.00885v1, 1 Oct 2026, NeurIPS 2026 Workshop on AI for Verifiable Coding; 9 pages of text, Appendices A to C (pp.12-18) with budgets, validation and the full prompts

proved, measured, trusted

The paper is about the step after a proof compiles: deciding whether to accept it. Its starting point (§1, p.1): “It does not, by itself, establish that an agent preserved the intended statement, avoided reference solutions, or submitted the same artifact that was subsequently reviewed.” The “it” is a successful Lean elaboration.

Nothing is proved about the harness. What is measured: solve counts, counts under a stricter axiom rule, counts from a second proof checker, tokens and dollars, for several coding agents with and without the harness on 100 Lean repository tasks (VeriSoftBench-Aristotle subset), 672 PutnamBench problems, and 2 Lean Eval developments. The paper also reports six observed threats to evaluation validity, each with the control it uses (Table 4, p.8); it does not say whose earlier runs they came from.

Trusted: the Lean kernel and toolchain; for some candidates also a second kernel (nanoda). The reviewer is an LLM and is not a proof; the paper says so (§7, p.9): “The reviewer shares the actor’s model family, so context separation does not establish independent errors.” and “Approval supplements kernel evidence.” The specification is outside all of it (Broader impacts, p.9): “Automated Lean proving can reduce verification effort, but proofs of inadequate specifications can create unwarranted confidence in unsafe systems.”

The author states the weakness of the evidence plainly (§7, p.9): “The evaluation is descriptive, with no repeated configurations, confidence intervals, or component ablations.” and “The unreleased harness limits external reproduction.” Inference: so no technique below has a controlled measurement of its effect; technique 5 has one single-run comparison that the paper does not call an ablation.

Terms. Actor: the coding-agent session that writes the proof. Reviewer: a new session that judges it. Candidate: the proof file submitted. Digest: the SHA-256 hash of the candidate. Frozen statement: the theorem text as given by the task, which the candidate may not change.

technique 1: a layered acceptance check that screens for the listed ways to compile without proving

What it is. A fixed sequence of mechanical checks run by the harness, not by the agent, each aimed at one way of making Lean accept a file that does not prove the task. The summary sentence (§3.6, p.4): “The layered verifier checks candidate syntax, preservation of the frozen statement, declaration shadowing, elaboration, and kernel axioms.”

When to use. On every candidate, before any reviewer or human sees it.

How it is done (§3.6, p.4; the actor prompt in Appendix C.2, pp.15-16, lists the same checks as shown to the agent).

1. Syntactic screen. Reject the file if it contains an admission (sorry, admit), an axiom declaration, a disallowed import (the PutnamBench actor prompt allows only import Mathlib), or a mechanism that lets compiled code stand in for a proof: native_decide, @[implemented_by], @[extern].
2. Statement comparison. The theorem statement in the candidate must equal the frozen one, ignoring whitespace and comments. Where the task supplies an answer value, that must be unchanged too.
3. Shadowing guard. Reject any new declaration that changes how a name used by the statement resolves, unless the declaration is already in the trusted template.
4. Elaboration. The file compiles with no errors.
5. Axiom audit. Run #print axioms on the target theorem; under the strict policy only propext, Classical.choice and Quot.sound may appear.
6. After acceptance, verify again, one candidate at a time, against a clean copy of the repository.

Why step 3 exists (§3.6, p.4): “This matters because redefining IsGreatest as set membership removes its upper-bound requirement while allowing an apparently unchanged theorem to elaborate.” The statement text is untouched; a name inside it now means something weaker.

Verus form. Inference: each layer has a Verus counterpart, and layers 2 and 3 merge.

• screen: reject assume(...), admit(), #[verifier::external_body], #[verifier::external] and assume_specification in agent-written code, outside an explicit allow-list
• frozen statement: the function signature with its requires and ensures, compared with the registered text
• shadowing: in Verus the weak point is the body of a spec fn that the ensures mentions. An agent that leaves ensures is_max(s, m) alone and edits spec fn is_max has done what the IsGreatest redefinition does. So the frozen text must include every spec fn reachable from the contract, and the check must reject both edits to them and new definitions of the same names in a nearer module
• elaboration: Verus reports the crate verified with no errors
• axiom audit: Verus has no command that lists the assumptions under one function, so the audit is a search over everything the function calls for the forms in the first bullet, including in dependencies

What does not carry over: #print axioms is computed by Lean from the proof term; the Verus search is textual and is only as complete as its list of escape forms.

Evidence.

• The audit finds assumptions that the benchmark’s own scoring ignores. Appendix A (p.12): “Twelve subset tasks can inherit disallowed axioms from repository lemmas.” Six depend on Lean.ofReduceBool or Lean.trustCompiler, six can inherit sorryAx from admitted dependencies. Hence two columns in Table 1 (p.5): with Opus 5 at xhigh effort, 100 of 100 tasks pass the benchmark rule with and without the harness, while 89 of 100 (Claude Code alone) and 96 of 100 (with the harness) pass the strict rule.
• None of the forbidden axioms came from the agent (Appendix A, p.12): “No additional agent-introduced axiom was identified in the audited candidates.”
• The check itself was tested (Appendix B, p.13): fifteen cases, covering admissions, declared axioms, native evaluation, extra imports, altered statements or answer values and several forms of shadowing, with positive controls such as a comment containing sorry. Result: “The tests exposed an incorrect rejection of template-defined answer abbreviations and a missed notation-based redefinition.” After the fixes, replaying 1,018 staged candidates recorded no false rejection.

Where it fails. The fifteen-case test found one hole (a redefinition through notation) in a check written to stop exactly that; the paper adds that the replay is “not a completeness guarantee for the verifier” (Appendix B, p.13). The paper reports no count of candidates that any layer rejected, so how often agents attempt these escapes is unknown.

technique 2: a fresh reviewer that sees the statement and the candidate, and nothing of how it was made

What it is. After the mechanical check passes, a new agent session reviews the candidate. It has read-only access, no transcript of the actor, no earlier reviews. It must recompile the candidate itself and return a verdict together with the digest of what it compiled.

When to use. For the defects a mechanical check cannot define: a proof that compiles and is vacuous or circular, or a weakening the screen did not anticipate.

How it is done (§3.4, p.3; reviewer prompts in Appendix C.1 and C.2, pp.14-17).

1. Start the reviewer only when a candidate has passed the verifier.
2. Give it the task statement and the candidate, read-only. Withhold the actor’s transcript, previous reviews and the orchestration state.
3. It recompiles the candidate once, through a reviewer-only tool that records the candidate’s hash.
4. It checks five things, in the paper’s words for “statement weakening, name shadowing, altered answer values, unsupported assumptions, and vacuous or circular constructions” (§3.4, p.3). The PutnamBench reviewer prompt spells out the last (p.16): “Are there vacuous or circular steps: a hypothesis that is never used because it was silently weakened, a ‘have‘ that restates the goal?”
5. It ends with exactly one verdict line, APPROVE or REJECT, and one digest line; on rejection it says what is wrong specifically enough to act on.
6. A rejection is written to a review file; the same actor session, with its memory, is resumed and told to check each finding against Lean before acting on it.

Two prompt sentences set the reviewer’s bias, one per direction. Against over-rejection (Appendix C.1, p.15): “Do not reject a kernel-checked proof merely for style.” Against over-approval (Appendix C.2, pp.16-17): “Approving a broken proof is the worst outcome available to you; rejecting a sound one merely costs a round.” The actor is told to treat the review as claims to test (Appendix C.1, p.14): “Treat its findings as hypotheses: check them against Lean and address every valid blocking issue.”

Verus form. Inference: the same session design applies unchanged: a second agent with the registered contract, the candidate file and a read-only Verus run. Its checklist in Verus terms: is the contract text the registered one; does any spec fn the contract uses differ from the registered one; is there an assume or #[verifier::external_body] the screen missed; is a requires so strong that no caller can meet it, or contradictory, so that the body verifies vacuously; does a loop invariant or decreases clause hold only because the loop never runs. What does not carry over: Lean’s reviewer is checking a proof of a fixed statement; a Verus reviewer also faces executable code, where the body may satisfy the contract and still not be the wanted program if the contract is weak.

Evidence.

• PutnamBench, Opus 5 at xhigh, one run (§5.2, p.6): “662 of 672 accepted candidates pass review in the first round, with the remaining 10 accepted in a second review round.” Mean reviewer cost $1.20perproblemagainst$3.52 for the actor, so review is about a quarter of the 4.72 total. - VeriSoftBench subset, Opus 5 at low effort with review (Appendix A, p.12): all 100 accepted, “71 in the first review round and the remainder within four”. - What the 10 and the 29 first-round rejections were about is not reported. Inference: the paper therefore gives no instance of the reviewer catching a wrong proof that the layered check had passed; the rejections may have been for real defects or not. Where it fails. Same model family as the actor, as quoted above. No ablation without the reviewer. And the reviewer's approval is only as good as the frozen statement it compares against. ## technique 3: bind verifier result, review and stored file to one hash What it is. Acceptance is a statement about one byte sequence. The rule (§3.4, p.3): “Acceptance requires a verifier pass and reviewer approval for the same artifact.” When to use. Whenever checking and storing happen at different moments, or an agent can write to the directory between them. How it is done (§3.4, p.3; §5.1.2, p.6; Table 4, p.8). 1. Compute SHA-256 of the candidate at submission. 2. The reviewer's compile tool records the hash of what it compiled; the reviewer copies that hash into its verdict. 3. Accept only if the submission's hash, the reviewer's hash and the hash of the file on disk agree. In the paper's words: “A mismatch invalidates acceptance.” 4. Use a new directory for each sample, never a reused one. 5. For multi-file work, copy the permitted files into a pristine workspace for each review and hash the complete candidate. 6. Protect the harness's own saved state: “An HMAC authenticates resumption state and binds it to the task and directory.” (§3.4, p.3). State that fails the check is quarantined. 7. The actor cannot write harness state or acceptance records (§3.1, p.3). The incident behind it (Table 4, p.8, and §6, p.8): stored and submitted proofs differed in 5 of 97 cases, because sample directories were reused. “Reused sample directories caused the proof on disk to differ from the proof submitted during the evaluated session.” Verus form. Inference: carries over without change, with one addition. For Verus the hash should cover the candidate file, the registered contract and `spec fn` text, and the toolchain identity, since a Verus result depends on the Verus and Z3 versions in a way a Lean kernel check does not (technique 9 is the paper's own case of a toolchain change breaking proofs). Evidence. The 5 of 97 figure is the only number; it measures the fault, not the fix. ## technique 4: restrict what the agent can read at run time, by the operating system, and log refusals What it is. The workspace holds only what the task allows; the restriction is enforced below the agent, not asked of it. The paper's name for the property is runtime blindness, with the caveat (§3.2, p.3): “This term makes no claim about the model’s training data.” When to use. Whenever a result is supposed to show the agent produced the proof, and a finished proof exists somewhere the agent could reach: the original repository, its history, another checkout, an earlier run's output, the public internet. How it is done (§3.2, p.3). 1. Build a sanitized project: proof bodies removed, and the target theorem withheld from retrieval. 2. Leave out any checkout that carries reference solutions. 3. For agents with a shell: an operating-system sandbox that applies to the whole process tree. 4. Network: a local CONNECT proxy that lets traffic reach the model provider only. 5. For agents without a shell: validate tool names and resolve path arguments before execution. 6. Cover alternative checkouts, repository history, previous outputs and the agent frontend's scratch state. 7. Log every access decision. Why a prompt or a settings file is not enough (§6, p.8): “A settings-based deny list was ineffective under permission-bypass execution, and restricting one checkout left other local copies and public network sources accessible.” Verus form. Inference: independent of the prover. For a Verus benchmark or product trial the withheld material is the reference `proof fn` bodies, loop invariants and `assert` statements, and any already-verified copy of the crate. Evidence (Table 4, p.8; §6, p.8). - Three access violations are listed (Table 4), each shown by reference similarity plus transcript or access records: similarity 0.99 to 1.00 and transcript path evidence after a permission bypass reached the reference repository; 1.00 and a recorded `curl`; 1.00 and recorded search paths after a filesystem search located another copy of the benchmark. The paper does not say whose runs these were. - With the proxy in place, agents kept trying. In the 100-task Numina-Lean-Agent run, “26 of 86 audited tasks issue a total of 425 requests to public code-hosting endpoints during solving, including github.com, codeload.github.com and raw.githubusercontent.com.” All were refused. - The paper does not claim those requests would have found answers: “The benchmark repositories are themselves public, so whether any request would have retrieved reference material is not established; the control removes the need to answer that question.” Where it fails. Training-data exposure is untouched (§7, p.9): “Runtime restrictions and similarity audits cannot rule out training-data exposure.” ## technique 5: retrieval tools that return statements without proofs What it is. A tool server over the Lean project offering lookup, search, usages and outline. The rule for its output (§3.3, p.3): “Responses contain declaration kinds, statements, and source locations without proof bodies.” When to use. When the agent must learn a repository's definitions and lemma statements, and reading whole files is costly or would expose proofs. How it is done (§3.3, p.3). 1. Separate two servers: general retrieval, and benchmark operations (start task, compile, submit). 2. Index declarations; answer with kind, statement and location only. 3. Shell-based agents may call the build directly, but acceptance still goes through technique 1 to 3. Verus form. Inference: an index over the crate and `vstd` that returns, for a name or a search string, the item kind (`spec fn`, `proof fn`, exec `fn`, `broadcast group`), its signature with `requires` and `ensures`, and its location. For a `spec fn` the body is part of its meaning and must be returned; for a `proof fn` the body can be withheld, which is the exact counterpart of the paper's rule. Evidence. - Motivation, from two exploratory runs (§3.3, p.3): navigation was 51 to 65% of tool calls and compilation 10 to 20%. The paper adds: “These exploratory counts motivate the interface without isolating its effect on success.” - One comparison, same harness and model (GPT-5.6 Sol, low effort, OpenCode frontend; §5.1.1, p.6): 67 of 100 tasks without the Lean tools, 70 of 100 with them, and cost down from 44.84 to 33.17. The no-tool transcripts contain 1,029 reads, 300 grep searches and 690 patches. Where it fails. A gain of 3 tasks in one run with no repeat. The same model in the Codex frontend with the harness solves 100, Inference: so the frontend mattered far more than the tools here; the paper says only that frontend behavior and tool integration both affect performance. ## technique 6: the harness decides when the task is over, and records why What it is. The agent ending its turn means nothing. Only a verifier pass ends a task; until then the harness resumes the same session with the latest diagnostics. Each task ends in one of several named states. When to use. With any agent that tends to stop early and report success, and in any evaluation where service failures happen. How it is done (§3.5, pp.3-4; continuation prompts in Appendix C.2, p.17). 1. Completion rule: “The framework determines task completion from verification evidence.” 2. If a turn ends without a verifier pass, resume the same session with the diagnostics and an instruction to continue. The actor is told so in advance (Appendix C.2, p.15): “Never end a turn having compiled cleanly without submitting.” 3. Keep external caps on rounds, time, spending and number of continuations. 4. Record the outcome as one of: accepted; review budget exhausted; resource cap reached; infrastructure interruption. 5. An authentication or usage error before any model spending leaves the task resumable and assigns no proof outcome. 6. A suspected false statement is handled apart from a failed proof. The actor prompt gives the method (Appendix C.2, p.16): “If you come to believe the statement is false, say so explicitly and try to derive ‘False‘ from its hypotheses – that is a real finding.” 7. Distinguish a continuation (same session resumed) from a fresh retry (new session); Appendix A (p.12) defines both. The actor prompt also carries a working method worth copying (Appendix C.2, p.16): “Turn each step of the sketch into a ‘have … := by sorry‘ and discharge them one at a time, compiling after each, so you always know which step is the one that is failing.” Verus form. Inference: the completion rule is the same: done means Verus verified the crate and the screen of technique 1 passed, never the agent's own report. The stepwise method maps to writing the intermediate facts of a proof as `assume(…)` lines first, so the function verifies, then turning them into `assert(…)` one at a time and rerunning Verus after each; the first one that fails is the step needing a lemma. The screen then guarantees no `assume` is left. A suspected false contract maps to trying to write a `proof fn` whose `requires` are the contract's preconditions and whose `ensures` is `false`. Evidence. - PutnamBench (Figure 3 and Appendix B, pp.7 and 13): 651 of 672 problems needed no continuation request and 21 did; a median of 7 compilations before the accepted submission, mean 8.9, maximum 56. - The cost of not doing step 5 (Table 4, p.8, and §6, pp.8-9): authentication errors generated 229 false failure records; in the Numina run, a spend limit and an expired credential produced tasks that used up their rounds with no model call and were recorded as proof failures. “Sixteen such records were identified by their zero token consumption and re-measured; all five of one batch then succeeded.” A scorer with missing dependencies marked five valid samples negative. Where it fails. The prompts tell the actor there is no limit while the runner enforces one; Appendix C.2 (p.15) says the statements about unlimited resources “do not replace the external stopping conditions enforced by the runner”. Whether that mismatch changes agent behavior is not examined. Cost can rise sharply: see the Fable 5 row under technique 8. ## technique 7: check accepted proofs a second time with a separate checker, and give it its own denominator What it is. Export the candidate and an independently built statement, compare them, and replay the proof in a different kernel implementation. When to use. For results that will be published or relied on, where a bug or a trick in the main toolchain's environment would otherwise go unseen. Steps of the checker, as Appendix A (p.12) gives them. 1. Build a trusted Challenge environment that contains only the target statement. 2. Build a separate Solution environment that contains the candidate, under a sandbox. 3. Export both with `lean4export`. 4. Require every declaration the statement refers to to agree between the two; inspect the exported axiom dependencies. 5. Check the solution with Lean and with the independent kernel nanoda. 6. Report the result over the candidates the checker could judge, not over all tasks. On reporting (§5.3, p.8): “These checks assess different properties, and incomplete independent-checker coverage should not be interpreted as either success or failure on the remaining tasks.” Verus form. Inference: does not carry over as built. Verus has no small independent checker that replays a proof; a Verus result is Z3 answering unsat on Verus's encoding. The nearest substitutes are weaker: rerun on a clean checkout, on a second machine, and under a varied solver seed. Step 4 does carry over and is the valuable part: build the contract in a workspace the agent never touched and compare it, item by item, with the contract in the agent's workspace. Evidence (Table 1, p.5; Appendix A, pp.12-13). The checker covers 72 of the 100 tasks, those in four repositories on Lean v4.24.0 or its release candidate (47 + 17 + 5 + 3 by Table 5). Results differ by configuration, for example 69 of 69 judged (harness, Opus 5, xhigh), 62 of 70 (harness, Fable 5, low) and 60 of 67 (harness with Codex, GPT-5.6 Sol, xhigh). On the rejections: “Among judged cases, no candidate is rejected on a task whose reference proof passes the same checker.” They concern axioms inherited from the repositories. Where it fails. 28 of 100 tasks are outside its reach, and some rows of Table 1 have no value. Lean Eval is the one setting where the benchmark itself demands it; both submissions passed. ## technique 8: report three success counts and the cost, not one number What it is. For each configuration: success by the benchmark's rule; success under the strict axiom rule; independent-checker acceptances over judged candidates; tokens and dollars including review and retries. When to use. When a benchmark is near its ceiling, or when configurations differ in budget. How it is done (§4, p.4; Table 1 caption, p.5). Fix model and effort within a comparison; state the requested protocol and admit where the recorded budget differed; include generation, review and retries in cost; mark which totals include recovery and later retries. Verus form. Inference: for a Verus benchmark the three counts would be: verified by the benchmark's command; verified with no escape forms anywhere under the target (technique 1's audit); verified again on a clean checkout with the contract rebuilt from the registered text. Evidence, the 100-task VeriSoftBench-Aristotle subset from 11 repositories (Table 1, p.5; the paper reports no repeated configurations). Given as benchmark-rule count, strict count, cost: - Opus 5, xhigh: Claude Code alone 100, 89, 135; with harness 100, 96, $111-Opus5,low:alone99,87,$101; with harness 100, 89, $118-Fable5,low:alone96,89,$157; with harness 100, 89, $350-GPT-5.6Sol,low,Codex:alone93,82,$69; with harness 100, 88, $62-GPT-5.6Sol,xhigh,Codex:alone97,86,$68; with harness 100, 88, $85-Numina-Lean-Agent,Fable5,low,itsownprotocol:86,strictnotreported,$2,011

So the harness raised the benchmark-rule count in four of five pairs and lowered cost in two of five. The paper’s summary (§5.3, p.8): “The results support configuration-dependent gains in efficiency, rather than a uniform reduction in inference cost.” The per-solved-task costs it gives check out: $2,011/86=$23.38, $350/100=$3.50, $157/96=$1.64.

PutnamBench (§5.2, p.6; Table 3, p.7): 672 of 672 accepted, Opus 5 at xhigh, one run, $4.72meanperproblem,$3,169 total, median wall time 27 minutes. Table 3 lists other systems also at 672 with reported mean costs from $0.17to$74; the paper notes they use different benchmark versions, models and budgets.

Lean Eval (§5.1.2 and Table 2, p.6; GPT-6 Astra): strong normalization for the calculus of constructions, 6 theorems, 233 files and about 28.6 thousand lines; quantifier elimination for real closed fields, 1 definition and 3 theorems, 1 file and about 1.5 thousand lines. The first had human help: “Its development includes operator assistance with checkpoints, infrastructure recovery, and strategic guidance.”

Where it fails. The subset is saturated; the paper says several configurations reach the ceiling and that it did not run the full 500 tasks (§5.1.1, p.6).

technique 9: after a toolchain upgrade, repair with an agent allowed to touch proof bodies only

What it is. Re-verify every accepted proof on the new toolchain; give the failures to an agent that may edit the proof body and nothing else; re-run the acceptance checks on each repair.

How it is done (Appendix B, pp.13-14). The evaluation ran on Lean v4.27.0; the benchmark moved to v4.33.1. All 672 accepted proofs were rechecked. An agent restricted to proof bodies repaired the failures. “Each repaired file was re-checked for compilation, permitted axioms, and an unchanged statement and answer term.”

When to use. On every prover or library upgrade of a verified code base.

Verus form. Inference: direct. On a Verus or vstd upgrade, rerun; for each function that no longer verifies, let the agent edit only proof { } blocks, assert statements, loop invariant and decreases clauses and proof fn bodies, with signatures, requires, ensures, spec fn bodies and executable statements frozen; then apply technique 1. What changes: in Verus a loop invariant is proof material but sits in executable code, so the frozen region has to be defined per syntactic item, not per file region.

Evidence. 502 of 672 compiled unchanged; 170 of 672 failed, all through changed tactic behavior (simp normal forms, ring_nf, instance synthesis); all 170 were repaired for $89.90intotal,about$0.53 each.

Where it fails. A quarter of accepted proofs broke across six minor versions; Inference: the paper reports the repair cost without asking whether proofs could be written to break less.

technique 10: screen for leakage by text similarity to the withheld reference

What it is. Compare each accepted candidate with the reference proof it was not supposed to see, and inspect the near-identical ones by hand.

How it is done (§3.6, p.4; Appendix A, p.13). Compute a raw-text sequence similarity ratio between the candidate and the reference. Ratios of 0.99 to 1.00 flagged the three confirmed access violations of technique 4. For other high ratios, read the transcript and see whether another model reproduces the proof. The paper’s caution (§3.6, p.4): “Similarity is a screening measure and does not by itself establish leakage or independence.”

When to use. After any benchmark run whose reference solutions exist on the same machine or online.

Verus form. Inference: unchanged; compare the agent’s proof annotations with the reference ones.

Where it fails. Short proofs and standard induction patterns score high without leakage (Appendix A, p.13); Inference: a leaked proof that was reworded would score lower, so a low ratio does not show independence (the paper says similarity does not establish independence).

inconsistencies in the paper

• Table 1’s row labeled OpenCode (67 solved, $45)isnotanunaidedagent.\S 5.1.1(p.6)andTable5(p.12)describethat67astheharnesswithOpenCodeandwithouttheLeantools.Sothe67to70pairmeasurestheretrievaltools,whileeveryotherpairinTable1measuresthewholeharness.-Table1givesthetargetprotocoloftheharnessrowsasPass@8withr=3.AppendixA(p.12)recordsdifferentbudgets:theOpusxhighharnessrunusedonesamplewithuncappedcompilation,andreviewedClaudeCoderunsuptofiveroundswithuncappedcompilation.Thecaptionconcedesthatrecordedbudgetsdiffer.Theharnessandunaidedrowsthereforedidnothaveequalcompilebudgets.-HarnesswithCodexatxhighis100inTable1and97inTable5.AppendixA(p.13)explains:96acceptedinitiallyof99available,1fromarecovereddependency,3fromfreshretries.TheunaidedCodexxhighfigureisalso97,sobeforefreshretriesthetwowereequal.-AppendixA(p.12)saysoneortwocandidatesperconfigurationareexcludedfromtheindependentchecker.Forthetwoharnessrowswith100solvedand69judged,72candidateswereeligible,so3wereexcluded.-Table4counts229falsefailurerecordsfromauthenticationerrors;\S 6speaksofsixteenzero-tokenrecordsre-measured.Howthesixteenrelatetothe229isnotsaid.-26of86auditedtasksmadeblockedrequestsinarundescribedas100tasks;why86wereauditedisnotstated(86isalsothatru{n}^{\prime }ssolvedcount).-ThePutnamBenchtotalsagree:$3.52 + $1.20=$4.72; $2,364+$805 = $3,169; 662 + 10 = 672; 651 + 21 = 672; 502 + 170 = 672.

already done; VL need not redo

• The acceptance protocol as a whole: mechanical screen, frozen statement, shadowing guard, axiom audit, transcript-blind reviewer, hash-bound acceptance, harness-controlled continuation. The prompts are printed in Appendix C and can be adapted directly.
• The catalogue of ways an agent evaluation goes wrong, each with an observed instance (Table 4).
• Not done: any ablation; any measurement of what the reviewer catches; release of the harness; anything on whether the specification is the right one.

threat to VL

Inference: moderate, and of a specific kind. The paper is Lean-only and its harness is unreleased, so it does not compete for Verus work directly. Its numbers show that by late 2026 unaided Claude Code and Codex runs (up to eight samples each) solve 93 to 100 of the 100 subset tasks under the benchmark rule and 82 to 89 under the strict rule, so proof-writing skill is not where a product can stand apart; the paper locates the remaining value in the acceptance protocol and the evidence trail, which is the same ground a product of agent-written verified Rust would claim. Everything in techniques 1 to 6 can be rebuilt for Verus from the paper’s description. What the paper leaves open, and a Verus product still has to solve, is the Verus counterpart of the axiom audit and of the independent checker, and any check on the specification itself.

techniques for the catalog

• layered acceptance check — screen for admissions, axioms and native-code escapes, compare the statement with the frozen one, reject shadowing declarations, compile, then audit the axioms the theorem depends on
• shadowing guard — reject any new declaration that changes what a name in the frozen statement resolves to, since the statement text can stay identical while its meaning weakens
• transcript-blind reviewer — a new read-only session that gets only the statement and the candidate, recompiles it, and returns approve or reject with the candidate’s hash
• hash-bound acceptance — accept only when the verifier result, the reviewer’s compile record and the file on disk carry the same SHA-256, with one directory per sample
• runtime blindness — remove proofs and reference copies from the workspace and enforce file and network limits with an operating-system sandbox and a provider-only proxy, logging refusals
• statement-only retrieval — lookup, search, usages and outline tools that return declaration kinds, statements and locations without proof bodies
• verifier-controlled continuation — the harness, not the agent, decides completion from a verifier pass and resumes the same session with diagnostics until then
• outcome taxonomy — record infrastructure interruptions and zero-spend turns apart from proof failures so they can be resumed, not counted
• independent re-check with its own denominator — rebuild the statement in a trusted environment, compare exported declarations, replay in a second kernel, and report over judged candidates only
• strict versus benchmark-rule counts — report success under the benchmark’s rule and under a stricter allowed-axiom rule side by side, since dependencies can carry admitted lemmas
• sorry-skeleton proving — write the proof sketch as intermediate claims each left open, then close them one at a time with a compile after each
• proof-body-only upgrade repair — after a toolchain change, let an agent edit proof bodies only and recheck statement, axioms and compilation for every repair
• reference-similarity screen — flag accepted candidates nearly identical to the withheld reference for manual inspection of how they were produced
• validate the validator — test the acceptance check on a fixed set of bypass attempts and harmless look-alikes, then replay stored candidates to look for false rejections

Last edited: 2026-10-13