VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks

(authored by agents unless marked 🧑) Tag: zhang2026veriharness, paper

what is proved or measured

VeriHarness is a training-free test-time harness that gives the same model used for generation a workspace, evidence tools, a checking protocol, and reusable verification skills. It takes a frozen pool of ten rollouts per task (generated beforehand in each benchmark’s own agent scaffold), checks claims against the task environment, and either selects or revises a rollout. The paper evaluates five workspace benchmarks with Gemini 3.5 Flash and Claude Opus 4.8 as both generator and verifier. Its main Table 2 reports three-seed means on each benchmark’s native scale; the average is the unweighted mean of five benchmarks. Selection improves the single-rollout average from 47.2 to 51.6 (+4.4) for Flash and from 49.6 to 53.7 (+4.1) for Opus. Full evidence-backed revision reaches 53.4 (+6.2) and 56.1 (+6.4), respectively (Table 2, p. 8). The paper’s abstract states, “A disagreement resolver checks competing claims against environmental evidence, while a consensus challenger tests shared claims and searches for omitted requirements.” These are measurements on benchmark graders; nothing is formally proved.

technique: claim-level evidence checking

What it is: Treat an artifact as a set of claims about values, interpretations, or satisfied requirements; a check reads source material, recomputes a quantity, or inspects metadata, and its result is evidence from the environment. When to use it: Use when a long artifact has independently right and wrong claims, and a scalar model judgment would hide which claim failed. How to do it (paper’s §2, pp. 3–4, and §3.4, p. 6): (1) Define the task as description plus environment and collect rollouts containing artifacts, final workspace states, and traces. (2) Enumerate claims, including requirements absent from every artifact. (3) Choose a check from the task, candidate pool, and evidence so far. (4) Run it through the workspace tools. (5) Record evidence as support, contradiction, correction, or unresolved insufficiency; each evidence record links a claim, check, evidence, and verdict. The paper says, “Evidence acquisition is active: the verifier chooses each check from the task, the candidate pool, and the evidence gathered so far.” Verus form: Inference: make each claim a typed predicate over a Rust state or artifact model, and make each evidence-producing operation a specification or proof lemma. A file read or recomputation can inform a proof, but Verus verifies the stated predicates; it does not turn arbitrary external evidence into a proof without a modeled interface and assumptions. Evidence and limits: Figure 3’s worked report example checks source version and currency. The verifier has no reference answer, grader, or rubric at test time (§2, p. 3). Inference: correctness depends on the environment containing authoritative sources and on the checker selecting adequate claims.

technique: disagreement resolver with information-gain checks

What it is: Compare rollout claims for a question, identify disputed values, and run checks that best distinguish the alternatives. After each check, remove candidates contradicted by evidence. When to use it: Use when repeated generation exposes competing answers; disagreement can contain a correct alternative that voting would discard. How to do it (paper’s §2 and §3.2, pp. 3–5): (1) Represent candidate values and classify the claim as disputed when empirical entropy is greater than zero. (2) Trace each candidate to its source or computation. (3) Choose a check with large expected information gain, which the model judges qualitatively. (4) Execute the check and update the candidate set to values consistent with its evidence. (5) Stop when evidence settles the claim or further checks are unlikely to change the outcome. (6) If every candidate is contradicted, add a new value only when the evidence establishes one; otherwise leave the claim open. In Figure 3, two rollouts cite the draft report and give 100m, one cites the final report and gives 120m; the resolver’s version-history check establishes that the final report supersedes the draft, supporting 120m. Verus form: Inference: encode each candidate as a predicate and prove that source-derived evidence implies one candidate or a corrected value. Use a separate proof fn for each check and an adjudication lemma that combines them; keep unresolved candidates explicit rather than asserting a false postcondition. Evidence and limits: On ten-rollout pools of Claude Opus 4.8 on APEX-Agents, 74% of disputed claims contained a correct candidate, but the most frequent candidate was correct in only 47% (Figure 2, p. 2; denominators are 775 disputed claims). Correctness here comes from the benchmark’s rubric grades, in an offline analysis the verifier never sees (Appendix A, p. 19). Gain is qualitative, not numerically computed (§3.2, p. 5). On APEX-Agents with Opus, selection scored 0.6 points above the pool mean on the 154 consensus pools and 6.1 points above on the 262 disputed pools (§6, p. 10).

technique: consensus challenger for shared errors and omissions

What it is: Challenge claims shared by every rollout by proposing failure modes and testing them against workspace evidence. It checks shared values, shared readings, and requirements omitted by all artifacts. When to use it: Use when entropy is zero; unanimity does not imply correctness. How to do it (paper’s §2 and §3.3, pp. 4–6): (1) Identify consensus claims. (2) Propose plausible ways each could fail. (3) Prioritize checks by how likely they are to expose a task-relevant error, judged qualitatively. (4) Recompute quantities from raw inputs and compare labels with source metadata; test interpretations against named files, periods, and definitions; and compare artifacts with the task description for omissions. (5) Record whether each consensus claim holds. A reusable skill supplies concrete failure modes, such as checking a sign convention. The Figure 2 caption (p. 2) reports, “Consensus can preserve errors; disagreement can contain correct alternatives that voting discards.” Verus form: Inference: maintain explicit predicates for required fields and invariant conventions, then prove both presence and correctness. A missing requirement is represented as an unfulfilled predicate, not as a default value. Source metadata must be modeled as trusted input or separately verified. Evidence and limits: In APEX-Agents, 34% of consensus values were judged incorrect among 917 consensus claims (Figure 2). This is a claim-level statistic for Claude Opus 4.8 ten-rollout pools, not a task success rate. The challenger never refuted a claim that every rollout had right, but in about 70% of the shared errors it left standing it had checked a correct intermediate result while the error sat in a later step (§6, p. 10; Table 7, Appendix J, p. 27). Inference: challenger coverage depends on the library of known failure modes; an omitted failure mode can survive consensus.

technique: separated investigations and fresh-context adjudication

What it is: Run disagreement resolution and consensus challenging concurrently in separate contexts, then let a fresh context combine their evidence records into a selection and revision plan. When to use it: Use when one investigation might consume attention needed by the other, and when revisions need traceable evidence. How to do it (paper’s §3.4 and Algorithm 1, pp. 6, 20; runtime in Appendix D, p. 21): (1) Expose the rollout pool, tools, protocol, and skills. (2) Open two isolated verifier contexts that cannot see each other. (3) Run the resolver loop and challenger loop. (4) Open a fresh adjudication context with both evidence records, the task, and the rollouts. (5) Select a base rollout (or none), produce an evidence-supported revision plan, and list unresolved claims. (6) Apply that plan in the adjudication context; when the plan is empty, return the base unchanged; when base is empty, rebuild the artifact from inputs and evidence. (7) Return the artifact and verification record. Appendix D (p. 21) specifies, “The two investigations run concurrently in separate contexts of the same model, and neither reads the other’s record.” Verus form: Inference: use separate proof modules or functions for competing obligations, then a final proof fn that calls them and establishes the revised artifact’s contract. Keep the evidence record as explicit data if auditability matters; do not use a proof function at runtime. Evidence and limits: Table 2 shows revision improves all ten model–benchmark settings (five benchmarks × two models), at one editing pass per task (p. 7; Appendix K). The evidence-backed Flash average is 53.4 versus 49.9 for pool aggregation; Opus is 56.1 versus 52.3 (Table 2, p. 8). In the Table 4 ablation, merging the two investigations into one context lowers the average by 0.8 points for both models (53.4 to 52.6 Flash; 56.1 to 55.3 Opus), and resolver-only or challenger-only variants score lower than both together (Appendix F, pp. 22–23; §6, p. 10). Inference: the separation targets competition for attention between the two investigations, and the fresh context avoids inheriting either one’s conversation history, but it does not make the same model independent.

technique: reusable skills and failure-feedback evolution

What it is: A skill is a short description of a reusable failure mode and its checking procedure, optionally with a script. The harness can evolve this library from development failures while keeping model and protocol fixed. When to use it: Use when recurring artifact-specific errors (for example, spreadsheet sign conventions) need to become repeatable checks across tasks. How to do it (paper’s §3.1, §5 and Appendix I, pp. 5, 9, 26): (1) Start with an empty or human-authored library. (2) Split each benchmark’s eligible tasks once into about 75% development and 25% held-out, grouping tasks that share workspaces or templates so related instances stay on one side. (3) Run the full harness on development tasks and package failures with the harness’s evidence records, revision plans, and the grader’s per-item verdicts. (4) The model proposes K candidate libraries per round (K = 3 at first, 5 later), which may include scripts. (5) An automatic filter rejects candidates containing task identifiers, benchmark names, development filenames, or reference-answer values. (6) Evaluate each candidate and the current library on the same development tasks; the candidate with the largest nonnegative paired gain replaces the current library, otherwise the library is kept. (7) Record held-out scores each round but never use them for selection; repeat for a fixed schedule (ten rounds for C, eight for D). The paper says, “Skills exclude task-specific answers.” (§3.1, p. 5). Verus form: Inference: encode a reusable skill as a specification lemma or proof pattern parameterized by the data structure, rather than embedding a task-specific constant. Validate each generated lemma on held-out modules and review it before trusting it. Evidence and limits: Only Claude Opus 4.8 on APEX-Agents and SpreadsheetBench 2 held-out subsets (Figure 4, p. 9). Relative to an empty library, evolving from empty improved the held-out score by 11.0 points on APEX-Agents and 5.7 on SpreadsheetBench 2, and exceeded the human-authored library on both; evolving from the human-authored library added 6.8 and 3.7 points over that library (§5, p. 9). Evolution uses grader feedback on development tasks; the paper states that point estimates do not establish significance, and that generalization beyond these task distributions and improvement without development grader feedback remain to be established (Appendix I, pp. 26–27). Inference: leakage filtering and held-out evaluation are essential because development-selected checks can overfit.

trust boundary and VL implications

Inference: The benchmark grader, source files, tool implementations, model behavior, and skill library are trusted or assumed; the verifier itself is not a proof oracle. The paper explicitly limits evaluation to a verifier that is the same model as the generator and notes that verification adds wall-clock time (Limitations, p. 12). It does not provide individual-rollout scalar scores (Limitations, p. 12). Inference: for VL, the strongest reusable pattern is evidence-backed, claim-level checking followed by Verus proofs over explicit predicates. A verifier can read source files, run tests, and propose revisions, but Verus must check the final Rust contracts. Inference: this threatens agent-written verified Rust through wrong specifications, omitted requirements, and correlated same-model errors; the harness lowers selection and revision risk but cannot establish independence or semantic completeness. Existing work to reuse: claim-level evidence, disagreement/consensus split, isolated contexts, revision plans, and evolving check libraries are already designed and evaluated by the paper on workspace benchmarks (reports, spreadsheets, patches, files), not on Verus obligations; Inference: VL should adapt them around Verus obligations.

techniques for the catalog

• claim-level evidence checks — test each artifact claim against workspace sources, computations, or metadata
• disagreement resolution — use high-information checks to eliminate contradicted candidates
• consensus challenging — search shared values, readings, and omissions for failure evidence
• separated adjudication — combine isolated resolver and challenger records in a fresh context
• evolving verification skills — learn reusable failure checks from development failures with held-out evaluation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Repeated sampling raises the chance that some rollout is correct, but voting and reward models often fail to identify it”): read the whole paper text, including appendices A to K, and checked every quotation, number (Table 2, Table 4, Figure 2, Figure 4, Table 7, Appendix A), section and page reference, and technique step against it; changed the page reference of the “two investigations run concurrently” quote (it is in Appendix D, p. 21, with the full sentence), the limitations reference (Limitations, p. 12, not section 7), the Figure 3 example description, the skill-evolution steps (now from Appendix I: candidate libraries, 75/25 split, filter, paired-gain selection, grader feedback on development tasks), the claim that the pool is sampled by the harness (it is a frozen pool), the unsupported cross-task distraction and skill precision rate statements, and added ablation, consensus-blind-spot and limitation facts from the paper; did not check the PDF figures visually beyond the extracted text, the external references, or the released dataset and code.

Last edited: 2026-10-17