SpecGuardBench: Can Coding Agents Construct Reliable Validation Harnesses from Natural Language Specifications?

Zhiqing Zhong; Mingyu Chen; Aoyang Fang; Yuzhong Zhang; Haoye Tian; Lionel Briand; Boxi Yu; Pinjia He

cs.CLOct 12, 2026

SpecGuardBench: Can Coding Agents Construct Reliable Validation Harnesses from Natural Language Specifications?

Authors: Zhiqing Zhong, Mingyu Chen, Aoyang Fang, Yuzhong Zhang, Haoye Tian, Lionel Briand, Boxi Yu, Pinjia He

Organizations: The Chinese University of Hong Kong, Shenzhen · Aalto University · Lero, the Research Ireland Centre for Software · University of Limerick ·

Abstract

As coding agents become more capable, tests remain the primary evidence for judging whether their code is correct. Yet passing available tests does not establish that an implementation satisfies its natural language specification. Reliable validation requires checks that faithfully capture the specification and scenarios that thoroughly exercise the code, but current benchmarks provide limited insight into whether agents can construct such evidence themselves. We introduce SpecGuardBench, a benchmark of 291 tasks from 13 real-world repositories, covering 8 types of verification logic such as functional postconditions and interaction protocols. Given a natural language specification, repository context, and a reference implementation, an agent constructs a validation harness comprising executable checks and test scenarios. The checks should reject implementations that violate the specification while accepting those that satisfy it, and the scenarios should thoroughly exercise the code. Across four proprietary and open-weight coding agents, none constructs a harness scored as faithful on the benchmark's implementations for more than 63% of the tasks. The bottleneck lies less in exploring test scenarios than in constructing checks that faithfully reflect the specification. Specifically, the agents show a clear tendency to write checks that mirror the reference implementation rather than the specification, and therefore reject implementations that the specification permits.

Figures & tables

Figure 1: Overview of SpecGuardBench task. Given a natural language specification, the repository, and a reference implementation, an agent constructs a validation harness of test scenarios and executable checks; the harness is judged on whether it accepts implementations that satisfy the specification, rejects those that violate it, and how thoroughly the scenarios exercise the relevant code.

Figure 2: Construction of a SpecGuardBench task. An LLM decomposes the FeatureBench specification into atomic specifications (a) and, for each, writes a candidate violating implementation with a differential witness (b). The candidate must pass the instance’s original test suite and diverge from the gold implementation on its witness (c), and the witnesses of neighboring specifications are run against it (d). A candidate is kept only when a second LLM confirms from these divergences that it violates the targeted specification alone.

Agent	Detection $\uparrow$	False Alarm $\downarrow$	Faithfulness $\uparrow$	Edge Cov. $\uparrow$	Cost
Codex / GPT-5.6-sol	81.8%	23.0%	61.9%	82.0%	$0.74
Claude Code / Claude Opus 5	65.3%	20.6%	50.2%	72.4%	$1.79
OpenCode / DeepSeek-V4-Pro	66.7%	26.8%	45.0%	75.1%	$0.43
OpenCode / GLM-5.3	74.2%	15.1%	62.9%	84.3%	$1.48

Table 1: Performance of four baseline coding agents on the 291 validation tasks of SpecGuardBench . Cost denotes the average cost per task in U.S. dollars.

Panel of Figure 5 — Figure 5: False alarms make up 42–60% of each agent’s failures (a), and for three of the four agents, most missed violations persist even on scenarios proven to expose the violation (b). A failure is attributed to scenarios only when replacing them with witness scenarios makes the checks reject the violating implementation and accept the gold one; the remaining missed violations are attributed to the checks.

	Gold reference $\rightarrow$ violating reference (%)
Agent	Detection $\uparrow$	False Alarm $\downarrow$	Gold Rejection $\downarrow$	Faithfulness $\uparrow$
Codex / GPT-5.6-sol	83 $\rightarrow$ 78	21 $\rightarrow$ 37	0 4 $\rightarrow$ 29	65 $\rightarrow$ 46
Claude Code / Claude Opus 5	66 $\rightarrow$ 33	19 $\rightarrow$ 38	0 4 $\rightarrow$ 31	52 $\rightarrow$ 21
OpenCode / DeepSeek-V4-Pro	70 $\rightarrow$ 67	23 $\rightarrow$ 48	15 $\rightarrow$ 41	52 $\rightarrow$ 28
OpenCode / GLM-5.3	75 $\rightarrow$ 44	12 $\rightarrow$ 24	0 0 $\rightarrow$ 12	68 $\rightarrow$ 39

Table 2: On the Lite Set, every agent shown the violating implementation as the reference loses 19 to 31 points of faithfulness and rejects the unseen gold implementation on 12–41% of the tasks. The gold-reference values are the main experiment restricted to these 100 tasks. Gold Rejection is the part of False Alarm on the gold implementation.

Panel of Figure 6 — Figure 6: Submission rate, detection rate, false alarm rate, and faithfulness rate on the Lite Set under the gold reference, at step budgets of 30, 50, and 80 steps.

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Type	A check must establish that	Counterpart	$n$ (%)
Functional postcondition	the return value satisfies a predicate over the inputs	postconditions ( ensures in JML, ACSL, and Dafny)	143	(49.1%)
Input validation	for inputs meeting a stated condition, the call raises a specified exception, returns a specified error value, emits a specified message or warning, or emits none of these	specification cases (JML normal_behavior and exceptional_behavior , ACSL behaviors, SPARK Contract_Cases )	52	(17.9%)
State postcondition	state that outlives the call, in the receiver, an argument, or the module, ends in a required relation to its state before the call or to the inputs	two-state postconditions ( \old in JML and ACSL, old in Dafny)	18	(6.2%)
Frame condition	the call leaves specified state unmodified, and a result required to be new shares no state with existing objects	frame clauses ( assignable , assigns , modifies ), \fresh , separation logic	14	(4.8%)
Interaction protocol	the function calls specified collaborators with specified arguments and multiplicity, or reads a value from a specified source	I/O specifications in separation logic, flow contracts (SPARK Depends )	32	(11.0%)
Call order	events within one execution occur in a specified order	temporal logic (LTL), typestate	2	(0.7%)

Appendix

Table 3: The eight types of verification logic, with the counterpart of each type in established verification logics and the number and percentage of the 291 specifications of SpecGuardBench that belong to each type.

Agent	Detection $\uparrow$	False Alarm $\downarrow$	Faithfulness $\uparrow$	Edge Cov. $\uparrow$	Cost
Codex / GPT-5.6-sol	83.0%	24.3%	63.4%	82.4%	$0.73
Claude Code / Claude Opus 5	62.6%	19.9%	50.5%	73.9%	$1.76
OpenCode / DeepSeek-V4-Pro	64.7%	25.5%	45.1%	73.7%	$0.43
OpenCode / GLM-5.3	75.5%	17.2%	62.5%	84.4%	$1.41

Appendix

Table 4: Performance of the four coding agents on the 291 validation tasks of SpecGuardBench , averaged over the 30 features instead of over tasks. Each metric is defined as in Section 3.1 , computed within each feature, and then averaged over the features with equal weight. Cost denotes the average cost per task in U.S. dollars.

	Gold reference $\rightarrow$ violating reference (%)
Agent	Detection $\uparrow$	False Alarm $\downarrow$	Gold Rejection $\downarrow$	Faithfulness $\uparrow$
Codex / GPT-5.6-sol	86.5 $\rightarrow$ 78.3	24.8 $\rightarrow$ 31.7	0 1.5 $\rightarrow$ 24.1	66.2 $\rightarrow$ 51.5
Claude Code / Claude Opus 5	64.3 $\rightarrow$ 40.6	19.8 $\rightarrow$ 35.8	0 5.3 $\rightarrow$ 28.7	49.6 $\rightarrow$ 25.2
OpenCode / DeepSeek-V4-Pro	75.7 $\rightarrow$ 72.2	22.2 $\rightarrow$ 51.6	16.4 $\rightarrow$ 43.1	57.3 $\rightarrow$ 30.6
OpenCode / GLM-5.3	80.5 $\rightarrow$ 49.2	14.2 $\rightarrow$ 29.2	0 0.0 $\rightarrow$ 13.3	70.9 $\rightarrow$ 42.1

Appendix

Table 5: Table 2 averaged over the 30 features of the Lite Set instead of over its 100 tasks. Each metric is computed within each feature and then averaged over the features with equal weight.

Agent	Detection	False Alarm	Faithfulness	Edge Cov.
Codex / GPT-5.6-sol	81.8 $\pm$ 5.9	23.0 $\pm$ 5.7	61.9 $\pm$ 8.0	82.0 $\pm$ 6.4
Claude Code / Claude Opus 5	65.3 $\pm$ 5.4	20.6 $\pm$ 4.5	50.2 $\pm$ 6.3	72.4 $\pm$ 6.6
OpenCode / DeepSeek-V4-Pro	66.7 $\pm$ 5.8	26.8 $\pm$ 7.1	45.0 $\pm$ 6.1	75.1 $\pm$ 7.7
OpenCode / GLM-5.3	74.2 $\pm$ 5.8	15.1 $\pm$ 4.6	62.9 $\pm$ 6.9	84.3 $\pm$ 4.7
GPT-5.6-sol $-$ GLM-5.3	$+$ 7.6 $\pm$ 6.6	$+$ 7.9 $\pm$ 4.4	$-$ 1.0 $\pm$ 6.8	$-$ 2.3 $\pm$ 4.1
DeepSeek-V4-Pro $-$ Claude Opus 5	$+$ 1.4 $\pm$ 5.4	$+$ 6.2 $\pm$ 5.4	$-$ 5.2 $\pm$ 5.5	$+$ 2.7 $\pm$ 4.2

Appendix

Table 6: Table 1 with 95% confidence intervals clustered by feature. The last three rows give the differences between the agents that Section 4.2 compares.

In the contracts	In the paper
certificate	validation harness
build_cases() , coverage cases	scenario generator, test scenarios
check_case(case)	executable checks
case	test scenario
target	the callable the scenarios invoke
gold implementation, gold patch	gold implementation

Appendix

Table 7: Names used inside the pipeline and the corresponding terms of the paper.

AI Coding Agents

AI coding agents use language models and software tools to plan, edit, test, and maintain code with varying levels of autonomy.

See all 310 papers

SpecGuard: Proving a Task Is Broken Before the Agent Cheats
Oct 6, 2026Param Biyani, Krishnamurthy DvijothamAI Agent Safety Software Engineering Agents
MATS · Google DeepMind
SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents
May 20, 2026Bingchen Zhao, Dhruv Srikanth, Yuxiang Wu +1Reward Hacking AI Coding Agents
Weco AI
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
May 26, 2026Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6LLM Agent Evaluation Formal Verification
CMU · Amazon · Work performed while at Amazon.

Oct 6, 2026J/K move · Enter open · S save

SpecGuard: Proving a Task Is Broken Before the Agent Cheats

Param Biyani, Krishnamurthy Dvijotham

MATS · Google DeepMind

AI Agent Safety Software Engineering Agents Formal Verification Reward Hacking

Open paper AskPDF arXiv

As autonomous coding agents get increasingly deployed, the risk that accidental or adversarially injected misspecifications in tasks lead to dangerous agent behavior is critical to address. Prior work has shown that agents given such tasks rarely flag the conflict and instead cheat, editing tests or hard-coding expected outputs, and the actions taken to cheat can cause real damage, such as deleting a security defense to make a corrupted test pass. It remains unclear whether such conflicts can be established with independently verifiable evidence before the agent acts. We present SpecGuard, which detects and formally certifies these conflicts between task intent and tests. Given only the task description and codebase, SpecGuard autoformalizes the intended behaviour into a Lean 4 specification. The tests are formalized independently, and the Lean kernel checks whether any implementation could satisfy both formalizations, producing a machine-checked certificate when none can. On conflicted SWE-bench tasks, SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1%, with a nearly five-fold lower conflict miss rate than model-based judgment. SpecGuard provides a pre-execution safety check that identifies reward-hacking opportunities through formal certification of task-level conflicts, before any agent behavior is observed. Our code is available at https://github.com/prmbiy/specguard.

Abstract

AI Coding Agents

Explore similar work

SpecGuard: Proving a Task Is Broken Before the Agent Cheats

SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization