From Verification Failures to Reusable Guidance for Coding Agents

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

cs.SESep 30, 2026

From Verification Failures to Reusable Guidance for Coding Agents

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

Organizations: University of Illinois Urbana-Champaign

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Experience is retained in executable semantics and verification procedures. Agents construct specifications and proofs. Validation examines programs, assumptions, and evidence. Feedback returns to the responsible stage. HumanEval also exports residual domain lemmas to Lean.

Semantics / kit	Pass	Concerns	Fail	Pass rate	Legit rate
Agent-authored / no kit	23	41	100	14.0%	39.0%
Supplied / no kit	37	36	91	22.6%	44.5%
Supplied / kit	97	67	0	59.1%	100.0%

Table 1: Historical HumanEval audits at the common Stage 2 endpoint, 164 tasks per arm. Legit combines Pass and Concerns . Resources, repairs, and attempt selection evolved during the campaign, preventing a controlled ablation. Final audit outcomes are reported separately.

Model	Rules	Generic	Kit	Kit–Rules	Kit–Generic
Luna	15/31	15/31	19/31	$+12.9\ [-9.7,35.5]$	$+12.9\ [-6.5,35.5]$
DeepSeek	17/31	18/31	16/31	$-3.2\ [-19.4,12.9]$	$-6.5\ [-22.6,9.7]$

Table 2: Frozen guidance comparison on swapped semantics. Differences and pointwise 95% paired bootstrap intervals are in percentage points, resampling 31 programs. Every original attempted cell remains in the denominator.

	Accepted attempts		Solved within four attempts
Semantics	Bare	Kit	Bare	Kit
Ordinary	107/124	111/124	31/31	31/31
Renamed	90/124	109/124	29/31	30/31
Swapped	73/124	92/124	24/31	30/31
All	270/372	312/372	84/93	91/93
	72.6%	83.9%	90.3%	97.8%

Table 3: KleverBench’s historical comparison. Attempt acceptance includes structural, coverage, and proof checks. Each base program appears under all three semantics. Counts retain failed attempts and timeouts.

Appendix figures & tables14 assets

Supplementary material from the paper’s appendix.

Appendix

Audit	Inputs and mechanical evidence	Judgment and independence boundary
Stage 2	Candidate code, K artifacts, task statement, canonical implementation as behavioral evidence, and available checker results	Fresh model session examines semantics, specifications, and extensions. Canonical behavior is visible, so this is informed review.
Stage 6	Prior audit and classification, frozen target/source identities, inventories, obligation correspondence, clean Lean build, and axiom checks in proof mode	Fresh session with the recorded producer model family. Treatment condition and prior review are visible. Adequacy, classification, and bridge judgments remain model decisions.

Appendix

Table 4: Historical audit protocol. Fresh sessions and read-only candidates separate audit from construction. The same model family is used and the treatment condition is visible. Empty-obligation tasks receive classification-only review.

Defect category	HumanEval tasks	Original	After retries	Clean accepted
		Defects detected
Weak postcondition	41, 53, 138	3/3	3/3	3/3
Unsupported bridge	54, 57, 120	2/3	3/3	3/3
Source/proof mismatch	8, 48, 42	3/3	3/3	3/3
Incorrect semantics	23, 49, 101	2/3	3/3	3/3
Total	12 pairs	10/12	12/12	12/12

Appendix

Table 5: The 24 original attempts include two capacity failures without reports. One additional attempt for each gives 24 completed judgments from 26 attempts. Every returned judgment matches the author-expert label. Clean acceptance is unchanged. All 24 packages passed their 28 K claims.

Model / sample	Contrast	Kit-only	Control-only	Exact $p$	Holm $p$
Luna original	Kit–Rules	8	4	.3877	.7754
Luna original	Kit–Generic	8	4	.3877	.7754
Luna recovery	Kit–Rules	8	3	.2266	.4531
Luna recovery	Kit–Generic	7	3	.3438	.4531
DeepSeek original	Kit–Rules	3	4	1.0000	1.0000
DeepSeek original	Kit–Generic	2	4	.6875	1.0000

Appendix

Table 6: Paired comparisons on 31 programs. Original attempts are primary. Holm correction uses two contrasts within each model or recovery supplement. The joint four-contrast primary correction gives 1.0 throughout. DeepSeek has no eligible recoveries.

Primary comparison outcome	Bare	Kit
Accepted	270	312
Rejected by pre-proof checks	66	34
Proof timeout	28	4
Proof error	8	22
All attempts	372	372

Appendix

Table 7: Disjoint reported outcomes. Individual pre-proof check failures can overlap within an attempt and should not be added to this table as additional outcomes.

Figure 2: Acceptance by the five original authored difficulty tiers in the principal comparison. Each tier combines all three semantics. Tiers 4 and 5 include nested loops and pipelines. The bars show observed proportions across 372 attempts per arm.

Acceptance constraint	Compatible archived bare instructions
Imports and claims only, no rule/syntax/configuration/context items	Explicitly stated. The agentic renderer incorporates these clauses.
Exact supplied program, symbolic initial state, no final existential weakening	Explicitly stated.
Coverage of required inputs	Weak preconditions requested, concrete coverage enforced by the checker.
Forbidden claim attributes	trusted , simplification , macro , alias , anywhere , owise , and priority are checked but not individually enumerated in that prompt.

Appendix

Table 8: Prompt/checker correspondence, reconstructed from the compatible source snapshot. Historical rendered prompts and generation HEAD are unavailable, so this reconstruction cannot establish their exact content.

Nine-program extension	Bare	Kit
Ordinary semantics	31/36	35/36
Renamed semantics	27/36	31/36
Swapped semantics	14/36	14/36
All	72/108	80/108

Appendix

Table 9: Separate September 4 report, after the language and prompt vocabulary had changed. These attempts are not pooled with the primary experiment.

	Selected initial runs		After targeted feedback
Example	Complete targets	Checked claims	Complete targets	Checked claims
HKG	6/6	15/15	6/6	15/15
DSToken	5/6	18/28	6/6	28/28
DSValue	2/2	5/5	2/2	5/5
Storage variable	1/1	2/2	1/1	2/2
Total	14/15	40/50	15/15	50/50

Appendix

Table 10: Selected historical smart-contract packages. Claim denominators use the final inventory. Recovered initial transfer and DSValue statements differ from their final versions, so these are not matched-claim completion rates. Follow-up completes one function target. Counts concern the scopes in the retained packages.

Selected initial activity	Input tokens	Cached input	Output tokens
HKG	157,550,964	154,774,528	422,205
DSToken	149,267,850	146,764,928	427,152
DSValue	12,624,914	12,379,136	55,618
Storage variable	10,883,735	10,631,936	45,900
Total	330,327,463	324,550,528	950,875

Appendix

Table 11: Recorded selected initial-run usage. Input includes cached input, and output includes reasoning tokens. Follow-up usage, human minutes, expertise, and the complete run census are unavailable. The source estimates $171.95 for the measured activity. A cost comparison with manual verification is unavailable.

Implementation	Operation	Claims
OptimismPortal2	proveWithdrawalTransaction	11
OptimismPortal2	finalizeWithdrawalTransaction	1
L1StandardBridge	finalizeBridgeETH	1
L1StandardBridge	finalizeBridgeERC20	1
L1ERC721Bridge	finalizeBridgeERC721	1
L1CrossDomainMessenger	relayMessage	1

Appendix

Table 12: Retained Optimism claims with positive backend proof records. Eleven withdrawal claims cover lengths 0–10, with independent symbolic 600-byte elements for nonempty arrays. The original six claims are counted once. Human review confirms the specifications and proofs under the documented input and execution assumptions.

Paired evaluator outcome	Tasks
Both patches pass	405
Both patches fail	85
Baseline fails, reviewed patch passes	8
Baseline passes, reviewed patch fails	2
Total	500

Appendix

Table 13: The stored evaluator reports give 407 baseline passes and 413 reviewed passes. The earlier tracker records 415 reviewed passes because it marks both regressions as solved. The supplement preserves and checks these two disagreements.

Study	Agent/model	Resources	Endpoint and exposure
HumanEval historical	Codex 0.144.6, GPT-5.6 Sol, xhigh	Per-task kit/semantics hashes, K 7.1.293, Lean 4.22.0	Stage 2 comparison, final Stage 6 separately. Development tasks, selected repairs.
HumanEval audit challenge	Codex 0.155.0-alpha.16.3, GPT-5.6 Sol, high	K 7.1.337, 24 isolated packages	Author-reviewed scopes and seeds. 24 original attempts; two capacity retries.
KleverBench Luna controls	Codex 0.149.1, GPT-5.6 Luna, high	Fixed fe49fb5 core, K 7.1.337	31 programs, three arms, one original attempt per cell. Four setup recoveries are separate.
KleverBench DeepSeek controls	Codex 0.149.1, DeepSeek-V4.1-Flash, high	Same task instructions, core and K image	31 programs, three arms, one original attempt per cell. Provider transport and $0.10 cash allocation differ.
KleverBench historical	Codex 0.149.1, GPT-5.6 Luna	Kit fe49fb5 , K 7.1.337	Four attempts, structural/coverage/proof checks. Exposure boundary unknown.
KleverBench extension	Same recorded Luna agent	Same kit, changed data/vocabulary	Separate nine-program cohort.

Appendix

Table 14: Configurations differ across studies. Recorded model aliases leave server-side snapshots unspecified. The supplementary registry supplies budgets, selection limits, and source links. Dated repairs and replays have separate provenance.

Kit snapshot	Skills	Bytes	Tokens	Distinct membership
Historical fe49fb5	8	111,020	24,966	Includes on-paper reasoning
Released 5de7a09	8	118,181	26,202	Includes client setup
Development 8a2f727	9	125,119	27,809	Includes both

Appendix

Table 15: Static sizes of the delivered Markdown skills and references. Tokens sum separately encoded files under tiktoken 0.14.0 and o200k_base , including publication redactions and excluding message framing. Shared references add no skills. These counts measure library size. Historical Luna loading records are unavailable.

Observed difficulty	Retained procedure	Evidence requested
Symbolic state differs from invariant	Compare computation, bindings, and framed cells before revising mathematics	Residual state and matching repaired invariant
Helper rule replaces source execution	Classify the extension by its effect and establish the connection	Bridge-free execution theorem over the full matched context
Precondition removes difficult inputs	Review the complete intended domain and test coverage inputs	Rejected exclusions and documented case splits
Storage addresses alias	Apply writes in execution order and include the same-slot case	Claims covering aliased and distinct locations
Exception occurs after a log	State the execution boundary and model rollback at the call level	Raw-state and call-level claims
Accepted remote job loses its connection	Retain session and task identifiers and recover evidence	Task status, cancellation, and downloaded logs

Appendix

Table 16: Examples of procedures retained from the development record. The mapping documents the content of the current kit, with no isolated causal estimate for an individual procedure.

Explore similar work

The reach of a verification tool decides its value: A controlled study of verification surface, artifact quality, and cost in AI coding agents
Aug 28, 2026Achint MehtaCoding Agents Self-Verification
The Verification Horizon: No Silver Bullet for Coding Agent Rewards
Jun 24, 2026Binghai Wang, Chenlong Zhang, Dayiheng Liu +10Coding Agents Response-Level Rewards
Qwen Team
ClayBuddy: A Framework, Evaluation, & Mitigation of Coding Agent Failures
Jun 13, 2026Kenneth Ge, Andre AssisCoding Agents Agent Harness
Anthropic Fellows Program · Constellation

Aug 28, 2026, cs.SEJ/K move · Enter open · S save

The reach of a verification tool decides its value: A controlled study of verification surface, artifact quality, and cost in AI coding agents

Achint Mehta

Coding Agents Self-Verification Web

Open paper AskPDF arXiv

Modern artificial-intelligence coding agents can be equipped with tools for checking their own work e.g. a linter, a boot probe, a shell, a screenshot tool. We call this set the agent's verification surface. This study asks whether increasing only that surface, with everything else held fixed, produces a matching growth in the quality of the software the agent ships. We built a minimal coding agent whose tool list is the single controlled variable and used it to implement 1,116 web applications across six models and eight tool configurations. A condition-blind human graded every application against a frozen rubric, and automatic probes stress-tested the API-observable behaviors. Verification's cheapest benefit arrives first, which is to make sure that the application comes up. Without any tools, about one build in seven fails to launch at all and a single boot probe removes nearly all of these failures at roughly 35 percent of a full shell's token cost, while the full shell multiplies the no-tools cost by 2.35. Screenshots help most where mistakes are visible (e.g. element placement, interaction), though even there the gain over a shell is modest and does not survive correction for multiple statistical comparisons. In cases where failures can only be measured rather than seen, such as keeping scrolling smooth over a 100,000-row list, screenshots add nothing. A verification tool improves the output artifact only where its reach covers the way the application actually fails.

Abstract

Explore similar work

The reach of a verification tool decides its value: A controlled study of verification surface, artifact quality, and cost in AI coding agents

The Verification Horizon: No Silver Bullet for Coding Agent Rewards

ClayBuddy: A Framework, Evaluation, & Mitigation of Coding Agent Failures