PaperlayerView exact revision on arXiv

Source-linked AI summary

From Verification Failures to Reusable Guidance for Coding Agents

Yuqing Zhai, Xiaohong Chen, Lingming Zhang, Sriram Vishwanath, Grigore Rosu

arXiv:2609.39022v1cs.SEcs.AIcs.LOcs.PL

TL;DR

Coding agents need to prove that programs satisfy specifications while checking that those specifications capture requested behavior. This paper combines executable K semantics with reusable verification procedures; HumanEval reaches 164/164 final audit PASS verdicts, while KleverBench comparisons are mixed across two settings.

  • Problem

    Agents must establish both that a program satisfies a stated property and that the property covers requested behavior, since proofs can leave inputs unexamined.

    Source: §1 · p. 1, §2.1 · p. 2

  • Method

    The approach combines executable K semantics with expert-curated procedures for constructing specifications, repairing proofs, and validating adequacy at inference time with fixed model weights.

    Source: §1 · p. 1

  • Results

    HumanEval achieved 164/164 final AI audit PASS verdicts after two repairs, while KleverBench kit comparisons with complete rules and equally long generic advice were mixed across two settings.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The mixed KleverBench results make procedure selection and the cost of guidance concrete questions for further experiments.

    Source: §1 · p. 2

    HumanEval shaped the semantics and instructions during development, so generalization requires frozen evaluation on unseen tasks.

    Source: §4 · p. 5

Abstract

from arXiv · show

Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of procedures for constructing specifications, repairing proofs, and auditing their adequacy. A human-guided development campaign on HumanEval, a benchmark of 164 Python programming tasks, achieves a 164/164 success rate with the semantics and the kit, measured by final AI audit Pass verdicts after two targeted repairs. To examine whether auditing detects problems that successful proofs leave unresolved, we construct 12 author-reviewed pairs of clean and defective packages. Every package passes its K proofs, and completed audits identify all defects and accept all clean packages. We then use KleverBench to test specification and proof construction for 31 programs with changed operator meanings. Comparisons with complete acceptance rules and equally long generic advice yield mixed results across two model and budget settings, motivating further work on selecting useful guidance within resource limits. Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas. We report progress, difficulties, and lessons toward agents that deliver programs with checkable correctness arguments.

1 INTRODUCTION

The paper asks how expert diagnosis of verification failures can guide agents in both proving properties and checking that specifications capture requested behavior. It combines executable K semantics with reusable procedures and evaluates them across HumanEval, auditing, KleverBench, and smart-contract proofs.

1 INTRODUCTION

  • The study investigates how curated procedures connect semantics, specifications, proof extensions, and adequacy checks alongside prior work on proof hints, refinement, consistency, and textual reflection.The related systems cited address these components in different combinations.Source: §1 · p. 1
  • The workflow retains expert diagnosis in shared K semantics and procedures for specification, proof construction, and validation, with model weights fixed at inference time.Its K definitions support concrete execution and symbolic proofs across language rules for assignments, loops, and exceptions.Source: §1 · p. 1
  • 164/164 HumanEval tasks received final AI audit PASS verdicts after two targeted repairs using the semantics and kit.On 12 author-reviewed clean/defective pairs, completed audits detected 12/12 defects and accepted 12/12 clean packages; each proportion had a 95% Wilson interval of 75.8–100%.Source: §1 · p. 2
  • KleverBench kit acceptance was 19/31 versus 15/31 with rules for GPT-5.6 Luna, but 16/31 versus 17/31 for DeepSeek-V4.1-Flash.All paired kit-effect intervals included zero, leaving mixed results across the two settings.Source: §1 · p. 2
  • Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas.The studies also expose specification requirements for storage aliasing and call-level rollback.Source: §1 · p. 2

2 PROGRAMS, SEMANTICS, AND PROOFS

The verification task has two parts: prove a property under declared semantics and predicates, and validate that those choices capture intended behavior. K supports execution and symbolic reasoning, while separating program-state transitions from mathematical obligations.

2.1 THE VERIFICATION TASK

  • Formalization chooses semantics and predicates, verification establishes the implication under declared assumptions, and validation checks correspondence to intended behavior; termination is a separate obligation.Equation 1 applies to terminating executions and targets partial functional correctness.Source: §2.1 · p. 2
  • A successful proof alone may miss requested behavior if inputs are narrowed or an added rewrite rule asserts the desired result directly.The workflow retains the source, translation, specification, proof extensions, and evidence; tests and independent audits examine correspondence with intent.Source: §2.1 · p. 2

2.2 EXECUTABLE SEMANTICS AND DOMAIN REASONING

  • K rewrite rules describe configuration transitions, enabling concrete execution and symbolic proofs with constraints and guarded circular reasoning that can summarize loops.A configuration organizes computation, variable environment, memory, and other runtime components; Figure 1 depicts feedback to the responsible stage and HumanEval's export of residual domain lemmas to Lean.Source: §2.2 · p. 2, Figure 1 · p. 3
  • For the summation loop, symbolic execution handles the state transition while integer arithmetic discharges why the loop summary is preserved.Separating these obligations makes a failed proof easier to diagnose.Source: §2.2 · p. 3
  • HumanEval uses Z3 for suitable domain implications and exports additional lemmas for agent proofs checked by Lean, while K execution proofs remain distinct.The stated trust boundary includes translation, semantics, K and solver integration, lemma translation, and Lean's kernel and permitted axioms.Source: §2.2 · p. 3

3 RETAINING VERIFICATION EXPERIENCE

The authors turn diagnosed failures into versioned, reusable procedures with applicability conditions and checking examples. The current kit organizes specification, proof, and audit work, with validation feedback and tool support shaped by observed failures.

3.1 FROM A FAILED ATTEMPT TO A REUSABLE PROCEDURE

  • Experts converted recurring proof failures and semantic discrepancies into revised rules, tests, and procedures, recording applicability conditions and checking examples for later agents.The staged campaign separated this curation process from work on an individual task.Source: §3.1 · p. 3
  • For below_zero, the kit directs agents to compare the residual computation, bindings, and framed state with the proposed invariant, then preserve mismatch and repair evidence.A proof-only replacement loop also requires an equivalence argument against the source program.Source: §3.1 · p. 3
  • The split_words repair expanded a whitespace predicate from four to all 29 CPython code points and added pinned versions, complete comparisons, boundary tests, and consumer replays.The example records provenance and checks, but its effect on later tasks is unmeasured.Source: §3.1 · pp. 3–4
  • The kit classifies proof extensions as definitions, derived lemmas, operational bridges, or trusted primitives, with full-guard derivations or machine-checked connection theorems required where applicable.This classification directs unsupported equations toward proof and overbroad bridges toward domain justification.Source: §3.1 · p. 4

3.2 THE CURRENT KIT AND PLUGIN

  • The current snapshot packages nine skills and a shared reference library; the released plugin has eight skills, with kprover distributed separately for proof requests and evidence retrieval.The workflow selects semantics, builds specifications and proofs, audits adequacy, and produces claims, scope documents, replay commands, and audit reports.Source: §3.2 · p. 4
  • Validation checks proof extensions, claim coverage, assumptions, and reproducible evidence, then returns a failed check to the responsible stage with a specific obligation.Client changes also address observed failures including timeouts, missing diagnostics, token collisions, and dropped connections after request acceptance.Source: §3.2 · p. 4

4 HUMANEVAL WITH SEMANTICS AND THE KIT

The HumanEval campaign builds and audits implementations, specifications, and proofs across 164 Python tasks. The revised artifact set reaches 164 final PASS verdicts after two repairs, while separate studies probe audit adequacy and recurring proof failures.

4 HUMANEVAL WITH SEMANTICS AND THE KIT

  • Across 164 tasks per arm, historical Stage 2 audits distinguish PASS, CONCERNS, and FAIL, while LEGIT combines PASS and CONCERNS.The evolving resources, repairs, and attempt selection prevent a controlled ablation; final audit outcomes are reported separately.Source: Table 1 · p. 4, §4 · p. 4
  • 164/164 revised HumanEval packages received final AI audit PASS verdicts after two targeted repairs, with fresh proof replays, negative controls, and independent repair audits.The two repairs address a primality theorem for task 59 and pinned CPython whitespace behavior for task 125; the other 162 packages retain historical evidence.Source: §4 · p. 4
  • HumanEval had already shaped the semantics and instructions, and repairs and continuations occurred during the campaign, so generalization requires frozen evaluation on unseen tasks.The two final repairs used a separately recorded toolchain and were accepted by an author expert under the review packet's stated assumptions.Source: §4 · p. 5
  • Completed audits detected all 12 seeded defects and accepted all 12 clean packages, although all 24 packages' K claims proved.Each proportion has a 95% Wilson interval of 75.8–100%; one defect used a local rule to bypass an incorrect body and fabricate its specified result.Source: §4 · p. 5
  • Historical packages expose recurring failures in invariant representation, input coverage, and helper-rule justification, which became the substance of the kit's procedures.The records include 212 domain obligations across 72 tasks, while 92 tasks have none.Source: §4 · p. 5
  • Shared semantics preserves language behavior across tasks; a repaired Python remainder rule and operand-sign tests corrected an earlier Euclidean result for 7 mod (−3).The semantics covers the Python subset exercised by the campaign, and KleverBench next examines claim construction under changed programs and semantics.Source: §4 · p. 5

5 KLEVERBENCH UNDER UNFAMILIAR SEMANTICS

KleverBench tests whether reusable procedures improve specification and proof construction under unfamiliar semantics, using acceptance checks and comparisons against controls. Historical results show an overall gain, while matched-control results are mixed and leave guidance selection under resource limits as an open question.

5.1 TASKS AND ACCEPTANCE CHECKS

  • KleverBench tests 31 programs under ordinary, renamed, and swapped semantics, where familiar operators can take changed meanings.Acceptance requires structural checks, input coverage, and K proofs; concrete coverage points reject preconditions that exclude required inputs.Source: §5.1 · p. 5

5.2 FROZEN GUIDANCE WITH MATCHED CONTROLS

  • The frozen comparison gives each of three arms one attempt per program, with complete rules shared across arms and equal-length generic advice or a fixed kit core added.The generic advice and kit additions each contain 2,145 tokens; arms share programs, semantics, checks, and time limits.Source: §5.2 · p. 5
  • On swapped semantics, Luna’s kit accepts four more programs than either control, while DeepSeek accepts one fewer than Rules and two fewer than Generic; all intervals include zero.Within-model Holm-adjusted paired p-values are 0.775 for Luna and 1.0 for DeepSeek.Source: Table 2 · p. 6, §5.2 · p. 6
  • In Luna’s setup-recovery supplement, accepted claims number 15/31, 16/31, and 20/31, with both kit-effect intervals including zero.DeepSeek has no eligible setup recoveries.Source: §5.2 · p. 6

5.3 HISTORICAL RESULTS AND FAILURE PATTERNS

  • 42 additional accepted attempts with the kit (+11.3 percentage points) in the historical comparison.On original tiers 4 and 5, acceptance rises from 43/108 to 73/108; tiers 1 through 3 improve from 227/264 to 239/264.Source: Table 3 · p. 6, §5.3 · pp. 6–7
  • Forbidden additions to the claims module fall from 28 bare attempts to zero kit attempts, while attempts excluding required inputs fall from 31 to 26.The comparison cannot separate instruction adherence, clearer emphasis, or procedural guidance as explanations for the reduction.Source: §5.3 · p. 7
  • The later nine-program extension raises acceptance from 72 to 80 across 108 attempts per arm, while swapped-semantics acceptance stays at 14/36 in both arms.Ordinary semantics improves from 31/36 to 35/36 and renamed semantics from 27/36 to 31/36.Source: §5.3 · p. 7

6 APPLYING THE KIT TO SMART CONTRACTS

The smart-contract studies apply the kit to EVM specifications and proofs, including transfer rollback behavior and pause properties. The results are scoped to retained packages, declared input bounds, and specified execution settings.

6.1 TARGETS AND COMPLETION

  • The retained inventory contains 14 final packages covering 15 function targets, with 44 target claims and six auxiliary claims supported by proofs and passing final audits.The initial selected runs report 14/15 complete targets; the final inventory is used as a retrospective denominator.Source: §6.1 · p. 7

6.2 WHAT THE TRANSFER PROOF TAUGHT US

  • The DSToken transfer package distinguishes raw-runtime execution from enclosing message-call behavior: a failed call rolls back storage and logs even when raw exceptional execution retains an earlier log.Reusable EVM guidance covers ordered storage writes and aliasing, zero-valued uninitialized storage, emitted memory slices, log prefixes, and failure order; this package fixes Byzantium and disables gas accounting.Source: §6.2 · pp. 7–8

6.3 PAUSE BEHAVIOR AND THE SUPPORTED INPUT DOMAIN

  • Human-reviewed proofs cover pause properties for six Optimism operations and four separate pause-dependency claims, under London semantics with unbounded gas and declared input bounds.The 20 proofs establish expected reverts, error payloads, and preservation of target state and initial logs; dynamic byte arguments satisfy length(b) ≤ 230.Source: §6.3 · p. 8

7 RELATED WORK

Related work spans reusable agent guidance, specification synthesis, verification feedback, and semantics-based program reasoning. This paper focuses on expert-curated procedures that connect executable semantics, generated specifications, proof extensions, and validation.

7 RELATED WORK

  • Prior agent-memory approaches retain feedback, extract experience, store executable skills, or maintain evolving contextual guidance; this work instead curates versioned procedures and references with expert involvement.The procedures guide operational-semantics proofs and specify evidence for mathematical summaries and proof extensions.Source: §7 · p. 8
  • Specification-generation and verification-feedback work motivates separating checker acceptance from adequacy audits and connecting executable semantics, summaries, and proof extensions.The cited work includes AutoSpec and SpecGen (Wen et al., 2024; Ma et al., 2024), nl2postcond (Endres et al., 2023), Lemur (Wu et al., 2023), AlphaVerus (Aggarwal et al., 2024), and VERINA (Ye et al., 2025).Source: §7 · p. 8
  • The approach builds on K semantics and KEVM, alongside work on premise selection, proof construction, and checker-feedback repair.The paper’s focus is reusable agent experience across language definitions, specifications, proof extensions, and validation.Source: §7 · pp. 8–9

8 LESSONS AND NEXT STEPS

The paper frames reusable guidance as procedures that specify what to inspect and what evidence should justify the next step. Its experiments provide baselines and identify validation and guidance-selection questions for future work.

8 LESSONS AND NEXT STEPS

  • Retained procedures connect diagnosed failures to applicability conditions and evidence requirements, from invariant mismatches to summary adequacy and proof extensions.Examples include comparing symbolic states and framed bindings, proving a theorem connecting a mathematical summary to the requested property, and checking rollback behavior.Source: §8 · p. 9
  • Controlled comparisons are mixed: Luna’s kit count is higher and DeepSeek’s lower, with every paired interval spanning zero.The authors propose procedure ablations, adaptive loading under several budgets, and transfer tests on task families selected after resources are frozen.Source: §8 · p. 9
  • All 24 audit packages prove their encoded claims, and completed audit judgments match author-reviewed labels across 12 selected clean/defective pairs.The authors identify natural defects, additional reviewers, repeated historical audits, and machine-checked translation and connection theorems as extensions.Source: §8 · p. 9
  • The supplement preserves frozen instructions, records, claims, grading logs, and scripts that check aggregates offline, while fresh runs require corresponding tools or services.Generative AI assisted the work, but the authors remain responsible for the final scientific claims and distinguish AI audit verdicts from formal checker judgments.Source: REPRODUCIBILITY STATEMENT · p. 9, AI USE STATEMENT · p. 9

A.1 HUMANEVAL DEVELOPMENT AND SECOND-PASS RECORDS

The HumanEval campaign records historical proof and audit outcomes, then reports targeted repairs that bring the selected set to 164 final AI audit PASS verdicts. A separate seeded-defect study tests whether audits detect adequacy problems even when K claims pass.

A.1 HUMANEVAL DEVELOPMENT AND SECOND-PASS RECORDS

  • At Stage 2, the kit arm records 97/67/0 PASS/CONCERNS/FAIL, versus 23/41/100 for agent-authored semantics and 37/36/91 for supplied semantics.Historical final Stage 6 audits contained 162 PASS and two CONCERNS; a benchmark-wide count of fully machine-checked intent adequacy is unavailable.Source: §A.1 · p. 12
  • 164/164 final AI audit PASS verdicts follow two targeted repairs to the selected HumanEval packages.The revised artifact set adds a Lean adequacy theorem for task 59 and repairs task 125’s whitespace predicate; the other 162 packages retain historical evidence.Source: §A.1 · p. 12
  • Task 59’s Lean adequacy theorem establishes primality, divisibility, and maximality for every integer n ≥2 under its guarded summary equations.K execution and Lean number theory are checked separately; transcription from K to Lean remains a trust assumption, and the program claim establishes partial correctness.Source: §A.1 · p. 12
  • Task 125’s versioned predicate matches all 29 whitespace members in CPython 3.12.3 with Unicode 15.0.0, checked across all 1,114,112 code points.Four symbolic claims and 96 concrete K cases pass; only task 125 adopts the new predicate.Source: §A.1 · p. 12

A.1.1 AUTHOR-REVIEWED SEEDED-DEFECT AUDIT

  • The frozen audit study used 12 accessible HumanEval tasks with scoped clean packages and paired seeded variants, assessed by one fresh-session audit per read-only candidate.Auditors lacked prior reviews, paired copies, seed labels, and producer narratives; sessions were capped at 20 minutes and K commands at 180 seconds.Source: §A.1.1 · pp. 13–14
  • 12/12 completed audits detect seeded defects and 12/12 accept clean packages, each with a 95% Wilson interval of [75.8, 100].The original 24 attempts detected 10/12 defects and accepted 12/12 clean packages; two capacity failures were retried, yielding 24 completed judgments across 26 attempts. All 24 packages passed their 28 K claims.Source: Table 5 · p. 13, §A.1.1 · p. 14
  • The seeded-defect sample is small, scope-selected, and artificial, and its protocol differs from historical Stage 6.It does not calibrate all 164 selected artifacts or replace human review of the two repairs; the separate repair packet review was not a full line-by-line proof audit.Source: §A.1 · p. 13, §A.1.1 · p. 14

A.2.1 FROZEN GUIDANCE CONTROLS

The appendix reports frozen guidance comparisons, historical benchmark results, semantics and adequacy checks, and smart-contract evidence with explicit scope boundaries. Results vary by model and evaluation, and retained proofs do not by themselves establish that specifications cover the intended behavior.

A.2.1 FROZEN GUIDANCE CONTROLS

  • The frozen comparison uses all 31 programs under swapped semantics, one attempt per program in each arm, and equal-length 2,145-token Generic and Kit advice blocks.Rules provide complete acceptance requirements; Generic adds planning, checking, and revision advice, while Kit adds fixed procedures for scope, invariants, circularity, residual inspection, and non-vacuity.Source: §A.2.1 · p. 14
  • Kit accepts 20/31 Luna candidates in the setup-recovery supplement, with Kit–Rules +16.1 points [−3.2, 35.5] and Kit–Generic +12.9 [−6.5, 32.3].The original 93 attempts remain primary; four Luna trials failed during installation before any model call, and the supplement intervals cross zero.Source: §A.2.1 · p. 15, Table 6 · p. 15
  • DeepSeek accepts 16/31 Kit candidates versus 17 Rules and 18 Generic; Kit–Rules is −3.2 points [−19.4, 12.9], and Kit–Generic is −6.5 [−22.6, 9.7].The exception-filtered analysis gives 14, 17, and 16 acceptances out of 27, but the primary analysis retains all original candidates.Source: §A.2.1 · p. 15, Table 6 · p. 15

A.2.2 HISTORICAL COMPARISONS

  • 11.3 percentage points [6.2, 16.7] is the overall 31-program historical difference; the nine harder-tier programs show 27.8 points [16.7, 38.0].Across 93 program–semantics configurations, the kit has more successful attempts in 34, the same in 53, and fewer in six; both arms solve 83 at least once.Source: §A.2.2 · pp. 16–17
  • Historical outcome attribution is limited: hypothetical acceptance counts change depending on whether timeouts or disjoint claims-only rejections are credited to the bare arm.Overlapping pre-proof subcategories prevent unique attribution, and the frozen comparison supplies controls for a fixed historical excerpt.Source: Table 7 · p. 16, §A.2.2 · p. 17

A.3 SEMANTICS TRANSFORMATIONS AND ADEQUACY CHECKS

  • Swapped semantics changes addition/subtraction, multiplication/division, and conjunction/disjunction while preserving comparison, modulo, and indexing meanings.For sum-up, a claim restricted to N < 1 misses the loop behavior at N = 1; finite supplied-input coverage checks reveal this omission without establishing a weakest precondition.Source: §A.3 · p. 18
  • The gold-post evaluation checks preconditions against coverage inputs and postconditions against executed positive states and perturbed negatives, while symbolic claims must separately prove.Agents may supply verification helpers, so their validity is an additional assumption to inspect; the bare-agent report records 71 delivered modules, 60 passing checks, and 41 proving within 300 seconds.Source: §A.3 · p. 18

A.4 SMART-CONTRACT SCOPE AND EVIDENCE

  • Smart-contract records distinguish proof, independent audit, and reference-judge verdicts; a judge PASS can still miss reference-domain coverage.Recovered records show different initial and final claim scopes, and estimating the kit’s incremental effect requires a matched no-kit comparison.Source: §A.4 · pp. 18–19

A.5 OPTIMISM PAUSE BEHAVIOR AND PROOF SCOPE

The Optimism case reports human-reviewed proofs for pause behavior under documented assumptions. Its claims are bounded by input and execution conditions, and later array-proof evidence was audited but not independently replayed.

A.5 OPTIMISM PAUSE BEHAVIOR AND PROOF SCOPE

  • Human review confirms specifications and proofs for the scoped pause behavior under the documented input and execution assumptions.The retained table counts eleven withdrawal claims for lengths 0–10, with independent symbolic 600-byte elements for nonempty arrays; the original six claims are counted once.Source: §A.5 · pp. 19–20, Table 12 · p. 20
  • The six operation claims use London semantics, direct implementation runtimes, empty call stacks, and positive-infinite gas with gas tracking enabled.Canonical ABI data, scalar ranges, account constraints, authorized bridge callers, and configured remote bridges remain assumptions; malformed calldata, finite-gas outcomes, and deployed proxies are outside scope.Source: §A.5 · p. 20
  • All 16 operation claims restrict variable byte arguments to at most 230 bytes, an input-helper restriction rather than a Solidity contract or raw-calldata bound.The final judge identifies the larger byte domain as the sole remaining reference-coverage gap and does not extend any claim beyond its written guard.Source: §A.5 · p. 20
  • The final array auditor validates saved positive proof records but does not independently replay them, and the audit reports SOUND-BUT-LIMITED with adequacy and replay-evidence gates failed.Four further positive proof records cover guardian timestamp writes and pause responses under storage, wiring, and timestamp assumptions, but do not compose with all six operations into one execution theorem.Source: §A.5 · p. 20

A.6 EXPLORATORY SWE-BENCH REVIEW

The exploratory SWE-bench review studies kit-guided inspection of baseline patches, while preserving missingness and distinguishing changed-patch evidence from benchmark-level resolution outcomes. Results include both reviewed improvements and regressions, with limited comparison evidence.

A.6 EXPLORATORY SWE-BENCH REVIEW

  • Across 470 tasks using kit fef0123, reviewed passes are 385 versus 380 baseline passes, with seven gains and two losses; a separate 30-task version has 28 versus 27 passes.Different tasks were assigned to the two kit versions, so these counts do not estimate a version effect.Source: §A.6 · pp. 20–21
  • Among 405 shared passes, review changes 86 patches, of which 60 are labeled candidate baseline issues and 26 are excluded.Three candidates have archived added-test confirmation; nine other reports describe execution checks, while 48 rely on source inspection or hand reasoning.Source: §A.6 · p. 21
  • Fresh targeted execution confirms six of nine selected behaviors, while two cases remain unresolved and Django 13569 confirms SQL compilation structure only.All nine reviewed patches pass focused checks, but gold misses some supported behaviors, so expected outcomes also require independent intent evidence; full official suites were not rerun.Source: §A.6 · p. 21
  • Sphinx 8056 and SymPy 12419 regressions reproduce: reviewed patches fail their original FAIL_TO_PASS tests while retaining tracked PASS_TO_PASS tests.Historical image identifiers are unavailable, preventing a byte-identical environment comparison; original reports remain the evidence for the other 498 tasks.Source: §A.6 · p. 21
  • In a separate selected Claude cohort, kit and ordinary review each resolve 33 of 44 completed tasks, with ordinary review averaging less time, fewer turns, and fewer output tokens.The paired test has p = 1.0, and equal caps permit unequal consumed compute; this cohort provides no persuasive evidence of a kit advantage.Source: §A.6 · pp. 21–22
  • The earlier exploratory cohort has incomplete arms and missing historical image identities; only 43 triples have one attempt per arm.Those triples record 32 kit and 31 ordinary-review successes, and the cohort remains separate from the 500-task comparison and its missing control.Source: §A.6 · p. 22

B DEVELOPMENT LESSONS IN THE CURRENT IMPLEMENTATION

The current implementation versions the development kit and supporting resources separately, while retaining workflow examples and static resource-size counts. The cited revision awaits benchmark evaluation.

B DEVELOPMENT LESSONS IN THE CURRENT IMPLEMENTATION

  • Static skill and reference counts measure library size, not historical loading: Luna loading records are unavailable.The counts separately encode files under tiktoken 0.14.0 and o200k_base, excluding message framing.Source: Table 15 · p. 22
  • The September 24 kit revision adds checked summary adequacy and pinned library-model comparisons, but awaits benchmark evaluation.The kit, released plugin, and historical treatment instructions are versioned separately, with hashes defining the update.Source: B DEVELOPMENT LESSONS IN THE CURRENT… · p. 23
  • Recorded workflow deviations include skipped, delayed, and producer-completed audits, which informed changes to artifact requirements and stage dispatch.The retained examples also identify tests for interrupted requests, slow compilation, unavailable storage, and audit-stage enforcement; they are outside measured benchmark cohorts.Source: B DEVELOPMENT LESSONS IN THE CURRENT… · p. 23
Loading 2609.39022v1…