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 · 

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.
Figure 3
AgentDetection ↑\uparrowFalse Alarm ↓\downarrowFaithfulness ↑\uparrowEdge Cov. ↑\uparrowCost
Codex / GPT-5.6-sol81.8%23.0%61.9%82.0%$0.74
Claude Code / Claude Opus 565.3%20.6%50.2%72.4%$1.79
OpenCode / DeepSeek-V4-Pro66.7%26.8%45.0%75.1%$0.43
OpenCode / GLM-5.374.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.
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 (%)
AgentDetection ↑\uparrowFalse Alarm ↓\downarrowGold Rejection ↓\downarrowFaithfulness ↑\uparrow
Codex / GPT-5.6-sol83 →\rightarrow 7821 →\rightarrow 370 4 →\rightarrow 2965 →\rightarrow 46
Claude Code / Claude Opus 566 →\rightarrow 3319 →\rightarrow 380 4 →\rightarrow 3152 →\rightarrow 21
OpenCode / DeepSeek-V4-Pro70 →\rightarrow 6723 →\rightarrow 4815 →\rightarrow 4152 →\rightarrow 28
OpenCode / GLM-5.375 →\rightarrow 4412 →\rightarrow 240 0 →\rightarrow 1268 →\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.
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

TypeA check must establish thatCounterpartnn (%)
Functional postconditionthe return value satisfies a predicate over the inputspostconditions ( ensures in JML, ACSL, and Dafny)143(49.1%)
Input validationfor 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 thesespecification cases (JML normal_behavior and exceptional_behavior , ACSL behaviors, SPARK Contract_Cases )52(17.9%)
State postconditionstate 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 inputstwo-state postconditions ( \old in JML and ACSL, old in Dafny)18(6.2%)
Frame conditionthe call leaves specified state unmodified, and a result required to be new shares no state with existing objectsframe clauses ( assignable , assigns , modifies ), \fresh , separation logic14(4.8%)
Interaction protocolthe function calls specified collaborators with specified arguments and multiplicity, or reads a value from a specified sourceI/O specifications in separation logic, flow contracts (SPARK Depends )32(11.0%)
Call orderevents within one execution occur in a specified ordertemporal logic (LTL), typestate2(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.
AgentDetection ↑\uparrowFalse Alarm ↓\downarrowFaithfulness ↑\uparrowEdge Cov. ↑\uparrowCost
Codex / GPT-5.6-sol83.0%24.3%63.4%82.4%$0.73
Claude Code / Claude Opus 562.6%19.9%50.5%73.9%$1.76
OpenCode / DeepSeek-V4-Pro64.7%25.5%45.1%73.7%$0.43
OpenCode / GLM-5.375.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 (%)
AgentDetection ↑\uparrowFalse Alarm ↓\downarrowGold Rejection ↓\downarrowFaithfulness ↑\uparrow
Codex / GPT-5.6-sol86.5 →\rightarrow 78.324.8 →\rightarrow 31.70 1.5 →\rightarrow 24.166.2 →\rightarrow 51.5
Claude Code / Claude Opus 564.3 →\rightarrow 40.619.8 →\rightarrow 35.80 5.3 →\rightarrow 28.749.6 →\rightarrow 25.2
OpenCode / DeepSeek-V4-Pro75.7 →\rightarrow 72.222.2 →\rightarrow 51.616.4 →\rightarrow 43.157.3 →\rightarrow 30.6
OpenCode / GLM-5.380.5 →\rightarrow 49.214.2 →\rightarrow 29.20 0.0 →\rightarrow 13.370.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.
AgentDetectionFalse AlarmFaithfulnessEdge Cov.
Codex / GPT-5.6-sol81.8 ±\pm 5.923.0 ±\pm 5.761.9 ±\pm 8.082.0 ±\pm 6.4
Claude Code / Claude Opus 565.3 ±\pm 5.420.6 ±\pm 4.550.2 ±\pm 6.372.4 ±\pm 6.6
OpenCode / DeepSeek-V4-Pro66.7 ±\pm 5.826.8 ±\pm 7.145.0 ±\pm 6.175.1 ±\pm 7.7
OpenCode / GLM-5.374.2 ±\pm 5.815.1 ±\pm 4.662.9 ±\pm 6.984.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 contractsIn the paper
certificatevalidation harness
build_cases() , coverage casesscenario generator, test scenarios
check_case(case)executable checks
casetest scenario
targetthe callable the scenarios invoke
gold implementation, gold patchgold implementation
Appendix
Table 7: Names used inside the pipeline and the corresponding terms of the paper.
More in this topic

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

Explore similar work

CardsList
Oct 6, 2026

SpecGuard: Proving a Task Is Broken Before the Agent Cheats

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.

Param Biyani, Krishnamurthy Dvijotham

MATS · Google DeepMind

AI Agent SafetySoftware Engineering AgentsFormal VerificationReward Hacking
AskPDF
May 20, 2026

SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents

As long-horizon coding agents produce more code than any developer can review, oversight collapses onto a single surface: the automated test suite. Reward hacking naturally arises in this setup, as the agent optimizes for passing tests while deviating from the users true goal. We study this reward hacking phenomenon by decompose software engineering tasks into three parts: (i) a natural language description of the specification (ii) visible validation tests that exercise specified features in isolation, and (iii) held-out tests that compose those same features to simulate real-world usage. Based on the specification and the visible validation test suites, a genuine agent would be able to generate a solution that can also pass all of the held-out tests. Therefore we use the gap in pass rates on these two suites to quantify reward hacking. Based on this methodology, we introduce SpecBench, a benchmark comprising 30 systems-level programming tasks ranging from short horizon tasks like building a JSON parser to ultra long horizon tasks like building an entire OS kernel from scratch. Large-scale experiments reveal a consistent pattern: while every frontier agent saturates the visible suite, reward hacking persists, with smaller models exhibiting larger gaps on holdout suites. The gap also scales sharply with task length: it grows by 28 percentage points for every tenfold increase in code size. Failures range from subtle feature isolation to deliberate exploits, including a 2,900-line hash-table "compiler" that memorizes test inputs. SpecBench offers a principled testbed for measuring whether coding agents build genuine working systems or merely game the test suites developers hand them.

Bingchen Zhao, Dhruv Srikanth, Yuxiang Wu +1

Weco AI

Reward HackingAI Coding AgentsSoftware Engineering BenchmarksLong-Horizon Agent Evaluation
AskPDF
May 26, 2026

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications. We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems targeting Verus, a verifier for Rust, and Verus-SpecGym, an agentic environment in which models interact with Verus, bash, & the filesystem to develop these specs. The central challenge is evaluation: expert-written reference specs are expensive to write, & LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specs can be executed as Rust code, & (b) testing them against official Codeforces tests & adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On Verus-SpecBench, the strongest model, Gemini 3.1 Pro, solves 77.8% of tasks, other frontier models solve 51.1--57.8% & OSS models reach only 21.5--25.5%. Our analysis of failure modes shows that model-generated specs can omit important input assumptions, accept incorrect outputs, & reject valid ones. We also find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that spec autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code, data, & logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym

Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6

CMU · Amazon · Work performed while at Amazon.

LLM Agent EvaluationFormal VerificationAI Agent BenchmarksAutoformalization
AskPDF