Spec-Driven PBT: Deriving Semantic Invariants from Code Specifications for Agentic Property-based Testing

Spec-Driven PBT: Deriving Semantic Invariants from Code Specifications for Agentic Property-based Testing

arXiv:2611.15920v1 [cs.SE] 11 Nov 2026

Aditya Shukla Georgian Partners

Kartik Gupta Georgian Partners

Ali Alavi Generative Models Inc.

Pashootan Vaezipoor Georgian Partners

Abstract Software is increasingly written by AI agents that autonomously produce an implementation from a user’s natural-language description (the specification), a practice known as agentic coding. Code is now produced faster than it can be reviewed, and code written this way has been shown to exhibit its own characteristic failure patterns. Property-based testing (PBT), a long-standing technique in which invariant properties of a program are checked against many generated inputs, has recently been revisited with LLM agents authoring the properties, thereby removing the high-effort derivation of invariants that has long hindered its adoption. Existing agentic PBT methods, however, derive these properties from the implementation alone (Code-driven PBT). Agentic coding presents an opportunity here: a thorough specification, whether a detailed prompt or a full product requirements document (PRD), has become central to the practice, yet its role in testing the resulting code remains underexplored. In this work, we study the value of the specification as a source of properties for testing agent-written code. Our key insight is that the specification, unlike the implementation, records what the code was meant to do, and invariants derived from it are not biased by how a particular implementation happens to do it. We propose Spec-Driven PBT, an agent that first expresses invariants in natural language from the specification and only then inspects the implementation to translate them into concrete tests. Across 25 applications from the ViBench dataset, Spec-Driven PBT finds a novel set of bugs that Code-driven PBT misses, while writing 2.4× fewer property tests. Though the two approaches surface a roughly equivalent number of bugs overall, there is little overlap: nearly 60% of the 169 total bugs are found by only one of them. Qualitatively, we find that the bugs unique to Spec-Driven PBT tend to violate documented product workflows whereas those unique to Code-driven PBT instead concentrate on implementation robustness, offering complementary value for bug discovery in agent-written code.

1

Introduction

Software is increasingly developed by AI agents that autonomously generate an implementation from a user’s natural-language description of the intended behaviour, a practice known as agentic coding. As of mid-2026, nine in ten professional developers use coding agents at least weekly [JetBrains Research, 2026], and a growing collection of benchmarks—ViBench [Zhong et al., 2026], Vibe Code Bench [Tran et al., 2026], BaxBench [Vero et al., 2025] and ProjDevBench [Lu et al., 2026]—assesses agents on constructing complete applications from nothing more than a requirements document. The specification has consequently become the main artifact a developer authors, and often the only one they examine in full. Two implications follow. First, human review has become the bottleneck: code is generated at a pace that mandatory human inspection cannot sustain [Monperrus, 2026]. Second, correctness has not advanced at the same rate: even frontier models regularly produce applications that are incomplete or incorrect [Zhong et al., 2026, Lu et al., 2026], and among the agent-authored NeurIPS 2026 Workshop on AI for Verifiable Coding.

Spec-Driven PBT

Source code

2 first derive invariants from spec alone

Specification API docs · PRD

then inspect the code refine / add more invariants

translate into Hypothesis tests

1

3

4

def test_p(x): assert inv(x)

invariants.md

triage genuine failures

run @given(...)

$ pytest

5

test_x.py

BUG_xxx.md

refine tests

refine NL invariants

Code-driven PBT

derive properties from code

Source code

write Hypothesis tests

1

2

properties

triage genuine failures

run @given(...)

3

def test_p(x): assert prop(x)

test_x.py

agent todo list, not a file

$ pytest

4

BUG_xxx.md

refine tests

re-read code, revise properties

Figure 1: Spec-Driven PBT (top) against the Code-driven PBT baseline (bottom). Spec-Driven PBT starts by deriving natural-language invariants from the specification alone, whereas Code-driven PBT derives properties directly from the implementation. Both methods then translate to Hypothesis tests, run pytest, and triage failures, with two feedback paths apiece.

patches that pass their tests on SWE-bench [Jimenez et al., 2024], nearly a third behave differently from the developers’ fix [Wang et al., 2026]. Code produced in this manner has also been found to display its own distinctive failure patterns. Empirical taxonomies of LLM-generated code identify recurring categories of defects particular to generated code [Tambon et al., 2025, Dou et al., 2024, Wang et al., 2025]; security vulnerabilities are widespread even in functionally correct output [Vero et al., 2025, Zhao et al., 2025, Deng et al., 2026]; and failure analysis for ViBench’s agent builds finds that a substantial proportion of failures in LLM-generated applications arise from omitted or misunderstood requirements rather than from implementation mistakes [Zhong et al., 2026]. What these defects share is that they leave behind code that runs, passes the tests created alongside it, and appears plausible when examined in isolation. Property-based testing (PBT) is an established technique well suited to defects of this kind [Claessen and Hughes, 2000, Fink and Bishop, 1997]: across 40 Python projects, each property-based test kills roughly 50 times as many mutants as the average unit test, even after controlling for coverage [Ravi and Coblenz, 2025]. A property is specified once and evaluated against many generated inputs, so an invariant such as “no user can read a record they were not granted access to” is tested across multiple inputs and sequences of operations without listing them manually. Its adoption has historically been constrained by the effort required to derive useful invariants, which practitioners identify as the most difficult part of the practice [Goldstein et al., 2024]. LLM agents have recently reduced this barrier by writing the properties themselves: given a codebase, an agent infers candidate invariants, generates tests in a PBT framework such as Hypothesis [MacIver et al., 2019], runs them, and triages the failures, and this approach has uncovered real bugs across widely used open-source packages [Maaz et al., 2025]. PBT provides a second advantage in this context; a property is a concise, human-readable description of what the code should do [Goldstein et al., 2024], so a collection of properties gives a reviewer something substantially shorter than the implementation to compare with the specification—a means of verifying agent-written code without reading it all. 2

Such agent-driven property-based testing, however, determines what to test from the code itself—its docstrings, comments and call sites. This approach works for a mature library whose documentation captures long-established intent. For an application newly generated from a requirements document, it means that the implementation is evaluated only against its own claims [Barr et al., 2015]: in essence, a rule that the code implements consistently but incorrectly will pass every test derived from it. We call this family of approaches Code-driven PBT. Agentic coding creates an opportunity here that Code-driven PBT does not exploit. A comprehensive specification, whether a detailed prompt or a complete product requirements document, has become the primary input to the practice, and it is the one artifact that captures what the code was intended to do rather than what it actually does. Prior work has demonstrated that grounding LLM-written unit tests in a specification is what makes them effective [Haeri and Ghelichi, 2026] and has extracted properties from task descriptions to guide code generation [He et al., 2025], but specification-based testing of agent-built applications remains underexplored. Our central insight is that invariants obtained from the specification are not biased by the behaviour of a particular implementation, and can therefore falsify behaviour about which the implementation is internally consistent. We introduce Spec-Driven PBT, an agent that first formulates invariants in natural language from the specification, and only afterward examines the implementation—using it to identify inputs, boundaries and operation sequences that could falsify those invariants, without regarding it as the oracle. The invariants remain as a standalone natural-language ledger that the agent updates as it works, allowing a reviewer to audit what was tested against the specification without reading either the implementation or the tests. We ask: when an LLM agent writes property-based tests for agent-written code, does deriving the oracle from the specification uncover bugs that codedriven testing misses, and which kinds? The two approaches turn out to generate different kinds of tests. Because a specification describes what users do, spec-derived properties tend to examine workflows: multiple users, a sequence of operations, a state reached through an unusual path. Because code explains how routines operate, code-derived properties test routines with adversarial inputs. Our contributions are as follows: • Spec-Driven PBT, a prompt-driven property-based testing agent whose information boundary places the specification before the code, and which preserves its invariants as a naturallanguage ledger alongside the tests (Section 3). • A direct comparison with Code-driven PBT across 25 ViBench applications, using the same model and tools, and with the failing tests from both methods pooled and linked to candidate bugs by a blind LLM reviewer. Spec-Driven PBT produces 2.4× fewer tests, and finds a net-new set of bugs missed by purely Code-driven PBT; with nearly 60% of the 169 distinct bugs detected by only one method (Section 5). • A qualitative analysis of what each method finds. Using case studies, we demonstrate that the bugs unique to Spec-Driven PBT are violations of documented product workflows about which the implementation is internally consistent, whereas those unique to Code-driven PBT relate to implementation robustness. For a bug detected by both methods, only the specification-anchored test determines which of two conflicting implementations is incorrect (Section 6).

2

Related work

Property-based testing PBT originates with QuickCheck [Claessen and Hughes, 2000], which replaced hand-picked test cases with a stated property and a generator of random inputs, and was proposed early on as a route to software assurance [Fink and Bishop, 1997]. Hypothesis brought the approach to Python with integrated shrinking and stateful testing [MacIver et al., 2019], and it is the framework both methods in this paper target. Practitioners value properties as executable documentation of intent, but identify finding good properties as the principal obstacle to adoption [Goldstein et al., 2024]. Our work addresses this obstacle by having an agent derive the properties, and by deriving them from the document in which intent is already written down. LLM-assisted test generation Language models are already used to write tests directly. They generate unit tests that compile and pass at usable rates but often assert too little [Schäfer et al., 2024], they supply the targeted inputs that search-based generators struggle to reach [Lemieux et al., 2023], 3

and they drive fuzzing campaigns that have found real defects in deep-learning libraries [Deng et al., 2023]. In each case the model produces test cases, not the general statement they check. Code-driven agentic PBT Recent work automates the whole of PBT with an LLM agent. Agentic PBT [Maaz et al., 2025] reads a package’s source and documentation, proposes properties, writes and runs Hypothesis tests, and triages the failures; PBT-Bench scores agents on the same task against injected defects [Jing et al., 2026]. Spec-Driven Test Generation [Tufano et al., 2026] has an agent write a function’s pre- and post-conditions before generating tests, but infers that specification from the code. In all three, a property asserts behaviour the implementation already exhibits or claims. We call this family Code-driven PBT, represented by Agentic PBT in our experiments. Specifications as test oracles A separate line of work supplies the expected behaviour from outside the implementation. Vikram et al. [2023] generate PBTs for single Python API methods from their documentation, without reading the implementation, and find that stating a property before implementing it yields better tests. He et al. [2025] derive properties from a task description to steer code generation, and Xiong et al. [2026] compile developer-written natural-language properties into executable checks for mobile applications. Most directly, Haeri and Ghelichi [2026] show on small Python functions that an LLM test author becomes effective when it is given an explicit specification of the intended behaviour, not merely the task description, and that an author who reads the code tends to treat its bugs as intended behaviour. Their author is handed a fixed, human-written list of rules and never sees the code. Ours derives its own invariants from a product requirements document for a complete application, then reads the implementation to find inputs that falsify them while the specification remains the oracle; this recovers the unspecified inputs that Haeri and Ghelichi note a rule-bound author cannot probe.

3

Method

Spec-Driven PBT is a lightweight approach that can be built on top of any coding agent. Through a natural-language prompt, the agent is instructed with the express goal of using property-based testing to discover bugs, rather than to write a comprehensive test suite. To that end, we instruct the agent to prioritize a small number of tests focused on bug-prone parts of the implementation. Figure 1 contrasts this workflow with Code-driven PBT; Appendix A gives the full prompt. Prompt

The agent is instructed to follow the below process:

1. Understand the specification – begin with the supplied specification, understand its core behavioral claims, and record an initial set of semantic invariants in an invariants.md file. Notably, the agent is firmly instructed to not peruse the codebase at this step. 2. Inspect the target system – now inspect the codebase, and locate bug-prone parts of the implementation, refining the invariants as needed but never treating the implementation as the oracle. 3. Prioritize the most promising invariants – focus on a few, high-impact properties that are likely to expose bugs. 4. Translate invariants into property-based tests – convert these invariants from natural language to idiomatic Hypothesis tests. 5. Run tests and triage failures – run the tests via pytest. For passing tests, try again with different Hypothesis configurations, input ranges and boundary conditions. For failing tests, verify that they do fail legitimately, and not because of a faulty test. 6. Produce bug reports – consolidate the valid failing tests into bug reports capturing the fault, the counterexample, steps for reproducibility, and a suggested patch. Key Design Choices Our primary design decision is setting the information boundary of instructing the agent to start with the specification first, and not explore the code at all. Spot checks had shown the agent writing tests closely coupled to the implementation even when the specification was provided, and this constraint de-biased it from over-indexing on the supplied implementation. This matches the finding of Haeri and Ghelichi [2026] that a test author who reads buggy code tends to treat the bug as intended behaviour, which is why they withhold the code from the tester entirely; we withhold it only until an initial set of specification-derived invariants has been recorded, so that it can still be used to locate falsifying inputs. The natural-language invariants.md ledger persists alongside the tests, recording what was tested and why without requiring us to read the tests. 4

Relation to Agentic PBT Our agent follows the same write–run–triage–report loop as Agentic PBT [Maaz et al., 2025], differing in the inputs it receives, the separately maintained natural-language invariants, and the constraint of deriving them from the specification before opening the source.

4

Experiments

ViBench Our primary testbed is ViBench [Zhong et al., 2026, ViBench Authors, 2026], whose applications are the setting this paper is about: each was built by a coding agent from a product requirements document (PRD), with no implementation constraints beyond the PRD itself. We use all 25 applications; Appendix D.1 describes the two releases and their generating models. ViBench carries no ground truth on bugs, so we verify findings by pooled blind review, described below. On this testbed Spec-Driven PBT receives the PRD and the code. Our Code-driven PBT baseline adapts the Agentic PBT method of Maaz et al. [2025] (Anthropic): it retains that method’s code-grounded prompt, adds the ViBench runtime instructions, and receives only the code. PBTBench As a secondary testbed we use PBTBench [Jing et al., 2026], 100 problem sets over 40 popular, human-authored open-source Python libraries, each carrying bugs injected by the benchmark’s authors. Because the injected bugs are known, PBTBench yields a ground-truth recall measure. Here both agents receive the library’s documentation as the specification; details are in Appendix C. Setup The two agents run under the following conditions: Claude Opus 5 through the Claude Code harness, with the Read, Write, Edit, Glob, Bash, Todo, WebSearch and WebFetch tools and internet access enabled. The agent’s workspace mounts the specification read-only under /inputs/specification (only for Spec-Driven PBT) and the code under /inputs/source, and writes its invariants, tests and bug reports to /output/. Isolating Specification-only vs. Code-only Grounding To isolate the effect of the source from which invariants are derived, we compared Spec-only and Code-only grounding of invariants on the same 25 ViBench applications. The two used the same model and environment, with prompts matched as closely as possible. Spec-only derived and froze its invariants from the PRD before inspecting code; Code-only did so from code alone. Both then used code to implement and run tests. In this setting, the composition of bugs between the two differed markedly, though Spec-only found fewer candidate bugs overall than Code-only. This suggested to us that deriving invariants from the specification could surface a net-new set of bugs, but also that restricting to the specification alone may leave useful properties unexplored. This motivated Spec-Driven PBT’s hybrid design: starting from specification-derived invariants, but also allowing the agent to add invariants after inspecting code. Appendix F reports this ablation. Blind review on ViBench Because both methods may surface the same underlying bug through different failing tests, we built a separate LLM Reviewer agent (Claude Opus 5) for evaluation only. For each application, the Reviewer receives the source, the PRD, and the failing tests of both methods with method labels removed, and judges each failing test on (i) whether the property being asserted is valid, (ii) whether the input range is reasonable, (iii) where the bug is present in the source, and (iv) which tests find the same underlying bug. Its output is a deduplicated list of candidate bugs. Qualitative analysis and manual validation We follow the qualitative-analysis protocol of ViBench [Zhong et al., 2026]. Concretely, one LLM agent (Opus 5) induces a taxonomy of underlying code faults from all candidate bugs. We then deployed a separate agent with this taxonomy to classify all the bugs found by only one of the two methods. Checking the robustness of LLM-applied labels, we found two repeat passes to agree on 98% of broad and 97% of fine-grained labels. We also manually validated a stratified subset of 25 candidate bugs with method labels withheld, assessing bug validity and comparing human and LLM taxonomy labels (Appendix E).

5

Results

Across the 25 ViBench applications, the Spec-Driven PBT agent authors fewer than half as many property tests as the Code-driven PBT baseline, yet a far larger share of them do useful work: 34% of its test functions are tied to at least one candidate bug, against 13% for the baseline, with our method taking a moderate edge in overall bugs found (Table 1). Notably, Spec-Driven PBT discovers 2.7× 5

as many candidate bugs per test (0.22 vs 0.08) as the baseline, and the two have similar false-alarm rates: the reviewer tied 193 of 204 failing tests to a bug for ours and 186 of 193 for the baseline. The two methods also find largely different bugs: of the 169 distinct candidates, 70 are found by both, 56 by Spec-Driven PBT alone and 43 by the baseline alone, a Jaccard index of 41%. We believe this difference in test efficiency to be reflective of the two methods’ overall designs. Since their prompts and workflows also differ, we cannot ascertain whether, or to what extent, specification grounding alone contributes to that difference. Appendix D reports efficiency and cost metrics. Table 1: Spec-Driven PBT (ours) against Code-driven PBT across two datasets. Test is a source-level test function or an exported Hypothesis state-machine case. Bugs means different things by dataset: ViBench carries no ground truth, so its figures are candidate bugs attributed by the blind reviewer. For PBTBench, these are injected bugs recovered under its strict fail-on-buggy, pass-on-correct (F→P) protocol, reported as recall over 365 injected bugs. Bug-bearing is the share of tests tied to ≥ 1 bug, by reviewer attribution on ViBench and by F→P confirmation on PBTBench. Dataset

Method

Tests

Bug-bearing

Bugs (recall)

Unique

Bugs/test

ViBench (25 PRDs)

Spec-driven Code-driven

566 1,384

34% 13%

126 113

56 43

0.22 0.08

321 (88%) 309 (85%)

33 21

0.14 0.10

Found by both: 70 of 169 distinct bugs (Jaccard 41%)

PBTBench (100 problems)

Spec-driven Code-driven

2,314 3,135

36% 25%

Found by both: 288 of 342 distinct bugs (Jaccard 84%)

On PBTBench, the picture is different. Spec-Driven PBT again discovers slightly more injected bugs, but the overlap in bugs found is much higher, with a Jaccard index of 84%. We hypothesize that this is largely due to the specification itself being more code-focused – since the API-reference style documentation typically covers function contracts rather than high-level requirements. Both agents also receive that documentation, so neither is advantaged by specification access. Some complementarity nonetheless remains: even where the specification adds little and both methods read the same code, directing the agent at the non-code artifact yields a slightly different set of bugs rather than a subset of what the baseline finds.

6

Discussion

6.1

Taxonomy of Surfaced Bugs

Following the qualitative analysis described in Section 4, Figure 2 characterizes the bugs each method found alone. It shows a marked difference between the two. State and Lifecycle and Logic and Computation failures comprise 61% of Spec-Driven PBT’s exclusive candidates, versus 31% for Code-driven PBT. Conversely, Input Handling failures comprise 49% of Code-driven PBT’s exclusive candidates, versus 16% for Spec-Driven PBT. The former includes bugs stemming from incorrect calculations, non-sensical lifecycle transitions, stale state, and destructive updates, while the latter are dominated by malformed or over-range values reaching a database, parser, or some other lower layer. These results do not imply that implementation robustness failures are unimportant or invisible. Rather, they expose a difference that aggregate counts conceal: specification-derived oracles contribute mostly product-semantic failures, code-derived oracles mostly implementation-boundary failures. The examples below make this concrete; full reports appear in Appendix I. 6.2 6.2.1

Bugs found only by Spec-Driven PBT Following a public account stays pending.

State and Lifecycle

Property In a photo-sharing application like Instagram, the PRD states that following a public account takes effect immediately. Our method read this as a behaviour that must hold between two accounts no matter their history. It then tested it by driving a pair of accounts, A and B, into each of six prior states – A never followed B, A already following B, A unfollowed B, A’s request declined while B’s account was private, A’s request still pending from when B’s account was private, and B 6

Spec-Driven PBT only (n=56) 13

Code-driven PBT only (n=43)

13

11%

12 4%

2 Access Control 11%

5%

5% 9 8

4

7%

Access Control 12%

Concurrency and Atomicity 9%

1

49%

7%

Logic and Computation

7%

34%

44%

Input Handling

State and Lifecycle 12%

7

State and Lifecycle

2% 2%

27%

11%

2%

10

3

Concurrency and Atomicity 12%

2%

5%

2%

16%

Logic and Computation 9

11

4%

Input Handling

10 9%

5%

12%

12

15

14

1

5

19%

7% 11% 8

6

7%

5%

6

12%

5

7

5%

2%

5%

4

3

2

Fine-grained classes 1

Unhandled input crash

6

Component contract mismatch

11

Non-atomic operation

2

Unenforced input constraint

7

Invalid state / relationship

12

Concurrent state divergence

3

Calculation error

8

Stale derived state

13

Unauthorized access / disclosure

4

Matching / filter semantics

9

Destructive / incomplete operation

14

Identity / credential mismatch

5

Position / boundary logic

10

Check-then-act race

15

Untrusted content / paths

Figure 2: Taxonomy of the candidate bugs found exclusively by each method. The inner ring gives abbreviated broad-class names; numbers beside the outer slices map the non-empty fine-grained classes to the legend. Percentages are computed within each method-exclusive set. Full definitions and counts appear in Appendix H. blocked A then unblocked. A then follows B, and the test checks both that the follow is accepted and that B’s posts reach A’s feed. @given(prior=st.sampled_from(PRIORS)) def test_following_a_public_account_takes_effect_immediately(prior): target, viewer = make_user("public"), make_user("public") post = target.create_post(caption="hello from a public account") _reach_state(viewer, target, prior) r = viewer.follow(target) assert r.json()["status"] == "accepted" rel = viewer.relationship_to(target) assert rel["following"] is True and rel["requested"] is False feed_ids = [p["id"] for p in viewer.get("/feed").json()["posts"]] assert post["id"] in feed_ids

Bug All of the six behaved as expected, barring one: when a follow request from A was still pending from when B’s account had been private, attempting to follow B once public returned pending again. The endpoint short-circuits on any existing row and echoes its status without consulting the target account’s current visibility, and switching an account to public rewrites that field without resolving the requests left behind it. The follower stays in requested and account B’s posts never reach A’s feed. 6.2.2

Accepted commits are silently lost.

Concurrency and Atomicity

Property In a source-control application like GitHub, the PRD states that a commit advances the branch’s tip and that history is append-only. Our method turned this into the requirement that every commit the API accepts must afterwards be reachable from the branch, and tested it with between two and five writers adding a file to the same branch at once. @CONC @given(n_writers=st.integers(min_value=2, max_value=5)) def test_every_accepted_commit_lands_on_the_branch(user, n_writers): repo = user.new_repo() user.write_file(repo, "main", "seed.txt", "seed\n") # ... writer(i) POSTs one commit creating f{i}.txt on main ...

7

responses = _run_parallel([writer(i) for i in range(n_writers)]) accepted = [r.json()["id"] for r in responses if r.status_code < 400] history = [c["id"] for c in user.get( f"/api/repos/{repo}/commits", params={"ref": "main"})["commits"]] missing = [cid for cid in accepted if cid not in history] assert not missing

Bug With only two writers, a commit was reported as created yet was absent from the branch’s history: the handler reads the tip without a row lock and then overwrites it, so the later write wins. The code-driven method also wrote race tests, but drew them from the concurrency guarantees the code documents about itself, covering starring, issue numbering and merging. The commit handler carries neither a docstring nor a lock, so there was no claim there for a code-derived oracle to check.

6.3

Bugs found only by Code-driven PBT

6.3.1

A malformed quantity crashes the cart.

Input Handling

Property In a storefront like Amazon, the API answers a bad request with a code and a message, and the listing routes already do so for a malformed stock count. Having read those routes, the Codedriven PBT agent tested that every endpoint taking a number honours the same contract, generating values a client might plausibly send for a quantity field. @given(qty=bad_counts) def test_unparseable_cart_quantity_is_a_client_error(api, seller, shopper, qty): listing = api.listing(seller, priceCents=500, stock=10) status, body = api.call(’POST’, ’/api/cart’, {’productId’: listing[’id’], ’qty’: qty}, shopper[’token’]) assert status == 400, body assert body[’code’] == ’INVALID_QTY’

Bug The cart, checkout and listing routes convert client-supplied numbers with a bare int() or a money parser and never guard the conversion, so a malformed value escapes as an unhandled exception and the server answers 500 rather than the 4xx its own contract promises. An empty quantity is worse than a crash: one route reads it as int(payload.get(’qty’) or 1), which silently substitutes a quantity of one and adds the item. Only reading the routes reveals that some of them validate and others do not.

6.3.2

A username is not stored as it was checked.

Access Control and Identity

Property In an events application, a member registers with a username and then signs in with it. Having read both the registration form and the model it writes to, the Code-driven PBT agent tested that the two agree: whatever username the form accepts must be the one the account is created under, and must then work at the login page. @given(username=unicode_usernames, email=emails, password=passwords) def test_registered_username_is_stored_verbatim(self, username, email, password): code = make_invite_code() response = self.client.post( ’/register/’, registration_payload(username, email, password, code.code)) assume(response.status_code == 302) self.assertTrue(User.objects.filter(username=username).exists())

Bug The form validates the string as typed, but the model normalises it before storing, so a username containing a character that changes under Unicode normalisation is saved under a different string than the one that was checked. The member cannot then log in, since the lookup uses what they typed, and the duplicate-username guard is bypassed for the same reason, so a second registration that should have been refused instead reaches the database and fails on the unique constraint. No product document describes normalisation; the property comes from noticing that two code paths disagree. 8

6.4

Bugs found by both methods

6.4.1

The same permission rule, written twice and disagreeing.

Logic and Computation

Property In a chat application like Discord, the PRD states that a member with the kick permission may remove another member, but not someone whose highest role outranks the actor’s. Importantly, an equal rank does not outrank. The rule is implemented twice, once in the flag that tells the client whether to show the kick button and once in the endpoint that performs the removal. The code-driven test asserts only that the two implementations agree with each other; ours checks the endpoint against the PRD first, and only then the flag against the endpoint. @given(actor_rank=ranks, target_rank=ranks) def test_can_be_kicked_matches_the_prd_and_the_endpoint(guild, actor_rank, target_rank): # ... give actor and target exactly the roles under test ... snap = actor.snapshot(sid) me = [m for m in snap["members"] if m["user_id"] == actor.user["id"]][0] them = [m for m in snap["members"] if m["user_id"] == target.user["id"]][0] prd_allows = (them["highest_position"] or 0) <= (me["highest_position"] or 0) resp = actor.req("DELETE", f"/api/servers/{sid}/members/{target.user[’id’]}") kicked = resp.status_code == 200 assert kicked == prd_allows # endpoint agrees with the PRD assert them["can_be_kicked"] == kicked # the flag agrees with the endpoint

Bug Both tests failed on the same counterexample: two members holding the default role of equal rank. The flag indicated that the target user could not be removed, while the endpoint allowed the removal anyways. Because the PRD makes an equal rank permissible, the endpoint was correct in allowing removal whereas the flag was incorrect in denying it. Anecdotally, we found that the bug fix suggested by the code-driven method would incorrectly have changed the endpoint to match the flag, satisfying the test while contradicting the requirement. In contrast, the fix suggested by our method correctly prioritized the behavior of the endpoint. This is the bias Haeri and Ghelichi [2026] report at function scale, observed here in a full application: with no external oracle, whichever copy the agent read first became the reference. This highlights the problem of purely code-driven tests: a supposed patch can resolve the failure it was shown and still diverge from what was actually wanted, producing incorrect behavior overall.

7

Limitations

Our primary limitation is the lack of ground-truth bug labels on ViBench, where we instead use LLM review to validate failing tests and deduplicate candidate bugs. Although our manual validation over a stratified subset supports the reviewer’s bug-validity judgments in all sampled cases, it does not necessarily establish its accuracy over the full corpus. Property-based testing is also not exhaustive: a suite that passes shows that the stated invariants held on the inputs tried, not that the implementation is correct, so nothing here argues that human review can be completely dispensed with. Finally, Spec-Driven PBT depends on the quality of the specification it is provided; it adds tangible value in the case of ViBench where the PRDs serve as thorough specifications, but we expect the method to degrade with a thin or stale specification.

8

Conclusion

Agentic coding produces, alongside every implementation, a specification of what that implementation was meant to do. Spec-Driven PBT puts that specification to work: an agent first derives naturallanguage invariants from the specification, then inspects the source code, where it may add or refine invariants and identify inputs that might falsify them. On 25 ViBench applications the method finds a novel set of bugs that Code-driven PBT misses. The two find largely different bugs: Spec-Driven’s are violations of the product workflows that the user asked for, whereas Code-driven’s are gaps in implementation robustness, so the approaches are complementary. Because each failing test is traced back to a derived invariant, its report can be interpreted in conjunction with the vocabulary of the specification that agentic coders already work in. More broadly, a ledger of natural-language invariants is a first step from an informal requirement toward a checkable property, and we see it as a natural stepping stone towards autoformalization pipelines. 9

Acknowledgments and Disclosure of Funding This work was conducted as part of the authors’ employment at their respective organizations. The authors received no external grant funding for this work.

References Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. The oracle problem in software testing: A survey. IEEE Transactions on Software Engineering, 41(5):507–525, 2015. doi: 10.1109/TSE.2014.2372785. Koen Claessen and John Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 268–279, 2000. doi: 10.1145/351240.351266. Junquan Deng, Zhiyu Fan, and Ruijie Meng. Understanding the (in)security of vibe-coded applications. arXiv preprint arXiv:2606.23130, 2026. Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang. Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 423–435, 2023. doi: 10.1145/3597926.3598067. Shihan Dou, Haoxiang Jia, Shenxi Wu, Huiyuan Zheng, Muling Wu, Yunbo Tao, Ming Zhang, Mingxu Chai, Jessica Fan, Zhiheng Xi, Rui Zheng, Yueming Wu, Ming Wen, Tao Gui, Qi Zhang, Xipeng Qiu, and Xuanjing Huang. What’s wrong with your code generated by large language models? An extensive study. arXiv preprint arXiv:2407.06153, 2024. Published in Science China Information Sciences, 2026; doi:10.1007/s11432-025-4632-8. George Fink and Matt Bishop. Property-based testing: A new approach to testing for assurance. ACM SIGSOFT Software Engineering Notes, 22(4):74–80, 1997. doi: 10.1145/263244.263267. Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. Property-based testing in practice. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE). Association for Computing Machinery, 2024. doi: 10.1145/ 3597503.3639581. Amin Haeri and Mahdi Ghelichi. Specification grounding drives test effectiveness for LLM code. arXiv preprint arXiv:2607.06636, 2026. Lehan He, Zeren Chen, Zhe Zhang, Xiang Gao, and Lu Sheng. Effective LLM code refinement via property-oriented and structurally minimal feedback. arXiv preprint arXiv:2506.18315, 2025. JetBrains Research. AI coding agents: Adoption trends. Developer Ecosystem Survey 2026, JetBrains Blog, August 2026. URL https://blog.jetbrains.com/research/2026/08/ ai-coding-agent-adoption-2026/. Accessed September 2026. Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. SWE-bench: Can language models resolve real-world GitHub issues? In International Conference on Learning Representations (ICLR), 2024. arXiv:2310.06770. Lucas Jing, Xinqi Wang, Liao Zhang, and Simon S. Du. PBT-Bench: Benchmarking AI agents on property-based testing. arXiv preprint arXiv:2605.15229, 2026. Caroline Lemieux, Jeevana Priya Inala, Shuvendu K. Lahiri, and Siddhartha Sen. CodaMOSA: Escaping coverage plateaus in test generation with pre-trained large language models. In IEEE/ACM 45th International Conference on Software Engineering (ICSE), pages 919–931, 2023. doi: 10.1109/ICSE48619.2023.00085. Pengrui Lu, Shiqi Zhang, Yunzhong Hou, Lyumanshan Ye, Chaoyi Huang, Zixi Chen, Ji Zeng, Hantao Jiang, Pengfei Liu, Yiwei Wang, and Ming-Hsuan Yang. ProjDevBench: Benchmarking AI coding agents on end-to-end project development. arXiv preprint arXiv:2602.01655, 2026. 10

Muhammad Maaz, Liam DeVoe, Zac Hatfield-Dodds, and Nicholas Carlini. Agentic property-based testing: Finding bugs across the Python ecosystem. In The 4th Deep Learning for Code Workshop at NeurIPS 2025, 2025. arXiv:2510.09907. David R. MacIver, Zac Hatfield-Dodds, and Many Other Contributors. Hypothesis: A new approach to property-based testing. Journal of Open Source Software, 4(43):1891, 2019. doi: 10.21105/joss. 01891. Martin Monperrus. The end of code review: Coding agents supersede human inspection. arXiv preprint arXiv:2606.13175, 2026. Savitha Ravi and Michael Coblenz. An empirical evaluation of property-based testing in Python. Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3897–3923, 2025. doi: 10.1145/3764068. Max Schäfer, Sarah Nadi, Aryaz Eghbali, and Frank Tip. An empirical evaluation of using large language models for automated unit test generation. IEEE Transactions on Software Engineering, 50(1):85–105, 2024. doi: 10.1109/TSE.2023.3334955. Florian Tambon, Arghavan Moradi Dakhel, Amin Nikanjam, Foutse Khomh, Michel C. Desmarais, and Giuliano Antoniol. Bugs in large language models generated code: An empirical study. Empirical Software Engineering, 30(3), 2025. doi: 10.1007/s10664-025-10614-4. Hung Tran, Langston Nashold, Rayan Krishnan, Antoine Bigeard, and Alex Gu. Vibe code bench: Evaluating AI models on end-to-end web application development. In Proceedings of the ACM Conference on AI and Agentic Systems (CAIS), pages 514–536. Association for Computing Machinery, 2026. doi: 10.1145/3786335.3813180. Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Y. Shi, Renyao Wei, Dorothy Chen, Franjo Ivančić, Livio Dalloro, and Pat Rondon. Grounding AI agents in contracts: An empirical evaluation of spec-driven test generation. arXiv preprint arXiv:2608.17177, 2026. Mark Vero, Niels Mündler, Victor Chibotaru, Veselin Raychev, Maximilian Baader, Nikola Jovanović, Jingxuan He, and Martin Vechev. BaxBench: Can LLMs generate correct and secure backends? In Proceedings of the 42nd International Conference on Machine Learning (ICML), volume 267 of PMLR, pages 61344–61390, 2025. arXiv:2502.11844. ViBench Authors. ViBench 1.5, 2026. URL https://vibench.ai/drafts/vibench-1-5/. Accessed September 2026. Vasudev Vikram, Caroline Lemieux, Joshua Sunshine, and Rohan Padhye. Can large language models write good property-based tests? arXiv preprint arXiv:2307.04346, 2023. You Wang, Michael Pradel, and Zhongxin Liu. Are “solved issues” in SWE-bench really solved correctly? An empirical study. In Proceedings of the IEEE/ACM 48th International Conference on Software Engineering (ICSE), pages 169–181, 2026. doi: 10.1145/3744916.3764576. Zhijie Wang, Zijie Zhou, Da Song, Yuheng Huang, Shengmai Chen, Lei Ma, and Tianyi Zhang. Towards understanding the characteristics of code generation errors made by large language models. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 2587–2599, 2025. doi: 10.1109/ICSE55347.2025.00180. Yiheng Xiong, Ting Su, Jingling Sun, Jue Wang, Qin Li, Geguang Pu, and Zhendong Su. From natural language to executable properties for property-based testing of mobile apps. arXiv preprint arXiv:2603.21263, 2026. Songwen Zhao, Danqing Wang, Kexun Zhang, Jiaxuan Luo, Zhuo Li, and Lei Li. Is vibe coding safe? Benchmarking vulnerability of agent-generated code in real-world tasks. arXiv preprint arXiv:2512.03262, 2025. Accepted to ICML 2026. Peter Zhong, Pashootan Vaezipoor, Fuyang Cui, Vaibhav Kumar, James Austin, Azin Asgarian, Toby Ho, Paul Inder, Imen Kedir, Zhen Li, Nicholas Ondo, Asna Shafiq, Ibrahim Sheikh, Edouard Sioufi, Setareh Soltanieh, Ben Wilde, Jacky Zhao, Ryan Carelli, Heather Miller, and Michele Catasta. ViBench: A benchmark on vibe coding. In Proceedings of the ACM Conference on AI and Agentic Systems (CAIS), pages 497–513. Association for Computing Machinery, 2026. doi: 10.1145/3786335.3813162. 11

Appendix A

Full Spec-Driven PBT prompt

Reproduced for one ViBench cell. A short runtime suffix is appended for context on spinning up the live application. Our agent’s container also carried a publicly available two-skill property-based-testing plugin that the baseline’s did not. No run invoked it: across all 50 generation traces the only tools used were Bash, Read, Write and Edit. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76

You are a **property-based-testing bug hunter**. Find a few genuine, consequential bugs, not broad test coverage. ## Target system **Source Code under test**: collabrative_kaban **Version**: Opus_4.6 **Scope**: ‘/inputs/source‘ (the complete library source tree) ‘‘‘text /inputs/ |--- specification/ # supplied product requirements document ‘--- source/ # target system implementation /output/ ‘‘‘ You may move back and forth between these steps as needed. You should exercise judgment about which promising leads deserve further investigation rather than treating the steps as a checklist. The installed skills are supporting guidance. If this prompt and an installed skill conflict, follow this prompt. ## Step 1 --- Understand the specification Begin with the supplied specification in ‘/inputs/specification/‘ (product requirements document). Understand its behavioral claims, then write an initial set of promising semantic invariants to ‘/output/invariants.md‘. During this step, work EXCLUSIVELY from ‘/inputs/specification/‘. Your first version of ‘/output/invariants.md‘ must be informed SOLELY by the supplied product requirements document. IMPORTANT: DO NOT inspect, search, open, or infer from ‘/inputs/source‘ (the source code under test) AT ALL until Step 2. ## Step 2 --- Inspect the target system Inspect the target system implementation in ‘/inputs/source/‘; freely add, remove, split, prioritize, or refine the invariants. The invariant file is working memory, not a frozen artifact or comprehensive checklist. The specification provides behavioral claims and the implementation helps locate promising ways to falsify them. Look especially for edge cases, sequences of operations, and interactions between otherwise valid features that could violate a documented requirement. Use the implementation to find inputs, boundaries, operations, and feature interactions, but never treat it as the oracle. ## Step 3 --- Prioritize promising invariants Focus on a few high-impact properties likely to expose genuine consequential bugs. Do not optimize for the number of invariants, tests, assertions, endpoints, or specification sections covered. Consult ‘pbt:property-based-testing‘ and ‘pbt:pbt-hypothesis‘ as needed for strong properties, independent oracles, Hypothesis strategies, shrinking, and stateful testing. Consult skill references selectively rather than treating a skills catalogue as a coverage checklist. ## Step 4 --- Turn invariants into bug-seeking PBTs Turn only promising invariants into bug-seeking property-based tests. During development, use focused pytest node IDs for the property currently being investigated; triage and refine immediately, and avoid repeated full-suite runs. A passing test is not evidence that the search is finished. For each promising property, actively seek valid inputs and operation sequences likely to falsify it. Preserve a failure only after confirming that the input is supported, the property is legitimate, and the behavior is reproducible. Do not modify or mutate the application to measure suite sensitivity. ## Step 5 - Test execution and bug triage Run your tests with ‘pytest‘.

12

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168

**For test failures**, apply this bug triage rubric: **Step 1: Reproducibility check** - Can you create a minimal standalone reproduction script? - Does the failure happen consistently with the same input? **Step 2: Legitimacy check** - Does the failing input represent realistic usage? - [yes] Standard user inputs that should work - [no] Extreme edge cases that violate implicit preconditions - Do callers of this code make assumptions that prevent this input? - Example: If all callers validate input first, testing unvalidated input is a false alarm - Is the property you’re testing actually claimed by the code? - [yes] Docstring says "returns sorted list" but result isn’t sorted - [no] Mathematical property you assumed but code never claimed **Step 3: Impact assessment** - Would this affect real users of the library? - Does it violate documented behavior or reasonable expectations? **If false alarm detected**: Return to Step 4 and refine your test strategy using ‘st.integers(min_value=...)‘, ‘strategy.filter(...)‘, or ‘hypothesis.assume(...)‘. If unclear, return to Step 2 for more investigation. **If legitimate bug found**: Proceed to bug reporting. **For test passes**, verify the test is meaningful: - Does the test actually exercise the claimed property? - [yes] Test calls the function with diverse inputs and checks the property holds - [no] Test only uses trivial inputs or doesn’t actually verify the property - Are you testing the right thing? - [yes] Testing the actual implementation that users call - [no] Testing a wrapper or trivial function that doesn’t contain the real logic ## Step 6 - Bug Reporting Only report **genuine, reproducible bugs**: - [yes] "Found bug: ‘json.loads(json.dumps({"(unicorn)": None}))‘ fails with KeyError" - [yes] "Invariant violated: ‘len(merge(a,b)) != len(a) + len(b)‘ for overlapping inputs" - [no] "This function looks suspicious" (too vague) - [no] False positives from flawed test logic **If genuine bug found**, categorize it as one of the following: - **Logic**: Incorrect results, violated mathematical properties, silent failures - **Crash**: Valid inputs cause unhandled exceptions - **Contract**: API differs from its documentation, type hints, etc And categorize the severity of the bug as one of the following: - **High**: Incorrect core logic, security issues, silent data corruption - **Medium**: Obvious crashes, uncommon logic bugs, substantial API contract violations - **Low**: Documentation, UX, or display issues, incorrect exception type, rare edge cases Then create a standardized bug report using this format: ‘‘‘‘markdown # Bug Report: [Target Name] [Brief Description] **Target**: ‘target module or function‘ **Severity**: [High, Medium, Low] **Bug Type**: [Logic, Crash, Contract] **Date**: YYYY-MM-DD ## Summary [1-2 sentence description of the bug] ## Property-Based Test ‘‘‘python [The exact property-based test that failed and led you to discover this bug] ‘‘‘ **Failing input**: ‘[the minimal failing input that Hypothesis reported]‘ ## Reproducing the Bug [Drop-in script that a developer can run to reproduce the issue. Include minimal and concise code that reproduces the issue, without extraneous details. If possible, reuse the mininal failing input reported by Hypothesis. **Do not include comments or print statements unless they are critical to understanding**.] ‘‘‘python [Standalone reproduction script] ‘‘‘ ## Why This Is A Bug [Brief explanation of why this violates expected behavior] ## Fix [If the bug is easy to fix, provide a patch in the style of ‘git diff‘ which fixes the bug,

13

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220

without commentary. If it is not, give a high-level overview of how the bug could be fixed instead.]

B

Full Code-driven PBT Prompt (Anthropic Agentic PBT)

‘‘‘diff [patch] ‘‘‘ ‘‘‘‘ **File naming**: Save as ‘bug_report_[sanitized_target_name]_[timestamp]_[hash].md‘ where: - Target name has dots/slashes replaced with underscores - Timestamp format: ‘YYYY-MM-DD_HH-MM‘ using ‘datetime.now().strftime("%Y-%m-%d_%H-%M")‘ - Hash: 4-character random string using ‘’’.join(random.choices(string.ascii_lowercase + string.digits, k=4))‘ - Example: ‘bug_report_numpy_abs_2025-01-02_14-30_a7f2.md‘ Save every bug report in ‘/output/bug_reports/‘. ## Step 7 -- Outcome Decision - **Bug(s) found**: Create bug report file(s) as specified above - you may discover multiple bugs! - **No bugs found**: Simply report "Tested X properties on [target] - all passed [yes]" (no file created) - **Inconclusive**: Rare - report what was tested and why inconclusive ## Step 8 --- Finish outputs Leave the evolving ‘/output/invariants.md‘, final tests under ‘/output/generated/‘, and any bug reports in place. The selected runtime instructions provide the one canonical final-suite command to run exactly once at the end. Copy the read-only ‘/inputs/source/‘ tree to the writable ‘/workspace/app/‘ before changing or running the application. Inspect its dependency metadata and the build-provided scripts (‘/workspace/app/setup-environment.sh‘ and ‘/workspace/app/start-server.sh‘), then use those scripts as appropriate. When a property needs persistence or a live service, start local PostgreSQL and set the application&#39;s documented database URL. You may use in-process tests where they independently cover the behavior; also use the live application for HTTP, persistence, authentication, user-facing workflows, or any other scenarios as you see fit. During development, use focused pytest node IDs for the property currently being investigated. Avoid repeated full-suite runs. After finishing all test authoring and triage, run the required complete suite exactly once. Write the final suite under ‘/output/generated/‘; do not modify ‘/inputs/‘. When finished, run this command exactly once and wait for it to finish: ‘‘‘bash pytest /output/generated -v --tb=short --junitxml=/output/final-pytest.xml ‘‘‘

This is the rendered prompt given to the Code-driven PBT baseline in one ViBench cell. It retains the Agentic PBT instructions of Maaz et al. [2025] and includes our ViBench runtime instructions at the end. For typesetting only, long lines are wrapped and non-ASCII symbols are transliterated; the instructions are otherwise unchanged. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26

--description: Property-based testing agent --# Property-Based Testing Bug Hunter You are a **bug-hunting agent** focused on finding genuine bugs through property-based testing with Hypothesis. Your mission: discover real bugs by testing fundamental properties that should always hold. ## Your Todo List Create and follow this todo list for every target you analyze: 1. [ ] **Analyze target**: Understand what you’re testing (module, file, or function) 2. [ ] **Understand the target**: Use introspection and file reading to understand implementation 3. [ ] **Propose properties**: Find evidence-based properties the code claims to have 4. [ ] **Write tests**: Create focused Hypothesis tests for the most promising properties 5. [ ] **Test execution and bug triage**: Run tests with ‘pytest‘ and apply bug triage rubric to any failures 6. [ ] **Report or conclude**: Either create a bug report or report successful testing Mark each item complete as you finish it. This ensures you don’t skip critical steps. You can use the ‘Todo‘ tool to create and manage your todo list. Use the ‘Todo‘ tool to keep track of properties you propose as you test them.

14

27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118

## Core Process Follow this systematic approach: ### 1. Analyze target - Determine what you’re analyzing from ‘‘/inputs/source‘ (the complete library source tree)‘: - Empty -> Explore entire codebase - ‘.py‘ files -> Analyze those specific files - Module names (e.g. ‘numpy‘ or ‘requests‘) -> Import and explore those modules - Function names (e.g. ‘numpy.linalg.solve‘) -> Focus on those functions ‘‘‘bash python -c "import numpy; print(’success - treating as module’)" python -c "from numpy import abs; print(type(numpy.abs))" ‘‘‘ ### 2. Understand the target Use Python introspection to understand the module or function you are testing. To find the file of a module, use ‘target_module.__file__‘. To get all public functions/classes in the module, use ‘inspect.getmembers(target_module)‘. To get the source code of a function, signature, and docstring, of a function ‘func‘ use: - ‘inspect.signature(func)‘ to get the signature - ‘func.__doc__‘ to get the docstring - ‘inspect.getsource(func)‘ to get the source code To get the file of a function, use ‘inspect.getfile(target_module.target_function)‘. You can then use the Read tool to read full files. If explicitly told to test a file, you **must use** the Read tool to read the full file. Once you have the file location, you can explore the surrounding directory structure with ‘os.path.dirname(target_module.__file__)‘ to understand the module better. You can use the List tool to list files, and Read them if needed. Sometimes, the high-level module just imports from a private implementation module. Follow those import chains to find the real implementation, e.g., ‘numpy.linalg._linalg‘. Together, these steps help you understand: - The module’s structure and organization - Function information, including signature and docstring - Entire code files, so you can understand the target in context, and how it is called - Related functionality you might need to test - Import relationships between files ### 3. Propose properties Once you thoroughly understand the target, look for these high-value property patterns: - **Invariants**: ‘len(filter(x)) <= len(x)‘, ‘set(sort(x)) == set(x)‘ - **Round-trip properties**: ‘decode(encode(x)) = x‘, ‘parse(format(x)) = x‘ - **Inverse operations**: ‘add/remove‘, ‘push/pop‘, ‘create/destroy‘ - **Multiple implementations**: fast vs reference, optimized vs simple - **Mathematical properties**: idempotence ‘f(f(x)) = f(x)‘, commutativity ‘f(x,y) = f(y,x)‘ - **Confluence**: if the order of function application doesn’t matter (eg in compiler optimization passes) - **Metamorphic properties**: some relationship between ‘f(x)‘ and ‘g(x)‘ holds, even without knowing the correct value for ‘f(x)‘. For example, ‘sin(pi - x) = sin(x)‘ for all x. - **Single entry point**: for libraries with 1-2 entrypoints, test that calling it on valid inputs doesn’t crash (no specific property!). Common in e.g. parsers. If there are no candidate properties in ‘/inputs/source‘ (the complete library source tree), do not search outside of the specified function, module, or file. Instead, exit with "No testable properties found in ‘/inputs/source‘ (the complete library source tree)". **Only test properties that the code is explicitly claiming to have.** either in the docstring, comments, or how other code uses it. Do not make up properties that you merely think are true. Proposed properties should be **strongly supported** by evidence. **Function prioritization**: When analyzing a module/file with many functions, focus on: - Public API functions (those without leading underscores) with substantive docstrings - Multi-function properties, as those are often more powerful - Single-function properties that are well-grounded - Core functionality rather than internal helpers or utilities **Investigate the input domain** by looking at the code the property is testing. For example, if testing a function or class, check its callers. Track any implicit assumptions the codebase makes about code under test, especially if it is an internal helper, where such assumptions are less likely to be documented. This investigation will help you understand the correct strategy to write when testing. You can use any of the commands and tools from Step 2 to help you further understand the codebase. ### 4. Write tests Write focused Hypothesis property-based tests to test the properties you proposed. - Use smart Hypothesis strategies - constrain inputs to the domain intelligently

15

119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210

- Write strategies that are both: - sound: tests only inputs expected by the code - complete: tests all inputs expected by the code If soundness and completeness are in conflict, prefer writing sound but incomplete properties. Do not chase completeness: 90% is good enough. - Focus on a few high-impact properties, rather than comprehensive codebase coverage. A basic Hypothesis test looks like this: ‘‘‘python @given(st.floats(allow_nan=False, min_value=0)) def test_sqrt_round_trip(x): result = math.sqrt(x) assert math.isclose(result * result, x) ‘‘‘ A more complete reference is available in the *Hypothesis Quick Reference* section below. ### 5. Test execution and bug triage Run your tests with ‘pytest‘. **For test failures**, apply this bug triage rubric: **Step 1: Reproducibility check** - Can you create a minimal standalone reproduction script? - Does the failure happen consistently with the same input? **Step 2: Legitimacy check** - Does the failing input represent realistic usage? - [yes] Standard user inputs that should work - [no] Extreme edge cases that violate implicit preconditions - Do callers of this code make assumptions that prevent this input? - Example: If all callers validate input first, testing unvalidated input is a false alarm - Is the property you’re testing actually claimed by the code? - [yes] Docstring says "returns sorted list" but result isn’t sorted - [no] Mathematical property you assumed but code never claimed **Step 3: Impact assessment** - Would this affect real users of the library? - Does it violate documented behavior or reasonable expectations? **If false alarm detected**: Return to Step 4 and refine your test strategy using ‘st.integers(min_value=...)‘, ‘strategy.filter(...)‘, or ‘hypothesis.assume(...)‘. If unclear, return to Step 2 for more investigation. **If legitimate bug found**: Proceed to bug reporting. **For test passes**, verify the test is meaningful: - Does the test actually exercise the claimed property? - [yes] Test calls the function with diverse inputs and checks the property holds - [no] Test only uses trivial inputs or doesn’t actually verify the property - Are you testing the right thing? - [yes] Testing the actual implementation that users call - [no] Testing a wrapper or trivial function that doesn’t contain the real logic ### 6. Bug Reporting Only report **genuine, reproducible bugs**: - [yes] "Found bug: ‘json.loads(json.dumps({"(unicorn)": None}))‘ fails with KeyError" - [yes] "Invariant violated: ‘len(merge(a,b)) != len(a) + len(b)‘ for overlapping inputs" - [no] "This function looks suspicious" (too vague) - [no] False positives from flawed test logic **If genuine bug found**, categorize it as one of the following: - **Logic**: Incorrect results, violated mathematical properties, silent failures - **Crash**: Valid inputs cause unhandled exceptions - **Contract**: API differs from its documentation, type hints, etc And categorize the severity of the bug as one of the following: - **High**: Incorrect core logic, security issues, silent data corruption - **Medium**: Obvious crashes, uncommon logic bugs, substantial API contract violations - **Low**: Documentation, UX, or display issues, incorrect exception type, rare edge cases Then create a standardized bug report using this format: ‘‘‘‘markdown # Bug Report: [Target Name] [Brief Description] **Target**: ‘target module or function‘ **Severity**: [High, Medium, Low] **Bug Type**: [Logic, Crash, Contract] **Date**: YYYY-MM-DD ## Summary [1-2 sentence description of the bug] ## Property-Based Test ‘‘‘python [The exact property-based test that failed and led you to discover this bug]

16

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302

‘‘‘ **Failing input**: ‘[the minimal failing input that Hypothesis reported]‘ ## Reproducing the Bug [Drop-in script that a developer can run to reproduce the issue. Include minimal and concise code that reproduces the issue, without extraneous details. If possible, reuse the mininal failing input reported by Hypothesis. **Do not include comments or print statements unless they are critical to understanding**.] ‘‘‘python [Standalone reproduction script] ‘‘‘ ## Why This Is A Bug [Brief explanation of why this violates expected behavior] ## Fix [If the bug is easy to fix, provide a patch in the style of ‘git diff‘ which fixes the bug, without commentary. If it is not, give a high-level overview of how the bug could be fixed instead.] ‘‘‘diff [patch] ‘‘‘ ‘‘‘‘ **File naming**: Save as ‘bug_report_[sanitized_target_name]_[timestamp]_[hash].md‘ where: - Target name has dots/slashes replaced with underscores - Timestamp format: ‘YYYY-MM-DD_HH-MM‘ using ‘datetime.now().strftime("%Y-%m-%d_%H-%M")‘ - Hash: 4-character random string using ‘’’.join(random.choices(string.ascii_lowercase + string.digits, k=4))‘ - Example: ‘bug_report_numpy_abs_2025-01-02_14-30_a7f2.md‘ ### 7. **Outcome Decision** - **Bug(s) found**: Create bug report file(s) as specified above - you may discover multiple bugs! - **No bugs found**: Simply report "Tested X properties on [target] - all passed [yes]" (no file created) - **Inconclusive**: Rare - report what was tested and why inconclusive ## Hypothesis Quick Reference ### Essential Patterns ‘‘‘python import math from hypothesis import assume, given, strategies as st

# Basic test structure @given(st.integers()) def test_property(x): assert isinstance(x, int)

# Safe numeric strategies (avoid NaN/inf issues) st.floats(allow_nan=False, allow_infinity=False, min_value=-1e10, max_value=1e10) st.floats(min_value=1e-10, max_value=1e6) # positive floats # Collection strategies st.lists(st.integers()) st.text()

# Filtering inputs @given(st.integers(), st.integers()) def test_division(a, b): assume(b != 0) # Skip when b is zero assert abs(a % b) < abs(b) ‘‘‘ ### Key Testing Principles - Use ‘math.isclose()‘ or ‘pytest.approx()‘ for float comparisons - Focus on properties that reveal genuine bugs when violated - Use ‘@settings(max_examples=1000)‘ to increase testing power - Constrain inputs intelligently rather than defensive programming - Do not constrain strategies unnecessarily. Prefer e.g. ‘st.lists(st.integers())‘ to ‘st.lists(st.integers(), max_size=100)‘, unless the code itself requires ‘len(lst) <= 100‘. ### Documentation Resources For a comprehensive reference: - **Basic tutorial**: https://hypothesis.readthedocs.io/en/latest/quickstart.html - **Strategies reference**: https://hypothesis.readthedocs.io/en/latest/reference/strategies.html - **NumPy strategies**:

17

303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346

https://hypothesis.readthedocs.io/en/latest/reference/strategies.html#numpy - **Pandas strategies**: https://hypothesis.readthedocs.io/en/latest/reference/strategies.html#pandas

C

Regenerating the PBTBench specifications

### Rare but useful strategies These strategies are uncommon, but highly useful where relevant. - ‘st.from_regex‘ - ‘st.from_lark‘ - for context-free grammars - ‘st.functions‘ - generates arbitrary callable functions Use the WebFetch tool to pull specific documentation when needed. --If you generate files in the course of testing, leave them instead of deleting them afterwards. They will be automatically cleaned up after you. **Remember**: Your goal is finding genuine bugs, not generating comprehensive test suites. Quality over quantity. One real bug discovery > 100 passing tests. Now analyze the targets: ‘/inputs/source‘ (the complete library source tree) ## Runtime Instructions Copy the read-only ‘/inputs/source/‘ tree to the writable ‘/workspace/app/‘ before changing or running the application. Inspect its dependency metadata and the build-provided scripts (‘/workspace/app/setup-environment.sh‘ and ‘/workspace/app/start-server.sh‘), then use those scripts as appropriate. When a property needs persistence or a live service, start local PostgreSQL and set the application’s documented database URL. You may use in-process tests where they independently cover the behavior; also use the live application for HTTP, persistence, authentication, user-facing workflows, or any other scenarios as you see fit. Iteratively run focused and full pytest commands. Repair invalid generated tests, imports, generators, or setup without weakening plausible application failures. Write the final suite under ‘/output/generated/‘; do not modify ‘/inputs/‘. When finished, run this command exactly once and wait for it to finish: ‘‘‘bash pytest /output/generated -v --tb=short --junitxml=/output/final-pytest.xml ‘‘‘

While preparing the PBTBench corpus we found that the documentation the benchmark ships as its specification sometimes states properties, invariants and even bugs outright. This matters because recall on PBTBench is scored against those injected bugs. An agent that reads such a passage can reach a defect from the prose rather than by testing for it, which inflates recall for any method given the documentation. We consequently do not use the shipped documentation. For every problem we regenerate an API reference from the library’s webpage. Every PBTBench figure in this paper is produced against that regenerated documentation. We share this updated set of documentation as part of our supplementary materials. D

Detailed results

The ViBench run at finer grain: the same 25 applications reported one at a time, then the two quantities the body states only in aggregate, namely how many bugs each test is worth and what each run cost to produce. D.1

The ViBench applications

The 25 PRDs the two methods were run against, by release. We use all fifteen ViBench 1.0 applications, implemented by Claude Opus 4.6, and all ten ViBench 1.5 applications [ViBench Authors, 2026], whose harder PRDs were implemented by Claude Opus 5. The two halves of the corpus were built by different models, so the implementations under test span two generations of agent-written code. 18

D.2

ViBench 1.0

ViBench 1.5

15 applications, Claude Opus 4.6

10 applications, Claude Opus 5

collabrative kaban creative community energy audit family friendly venue family social furniture freight hvac mafia

amazon-prime asana discord figma github

market place monopoly online whiteboard pilot logbook slack srm wedding

google-docs instagram jira uber youtube

Per-application results

These counts also bound how much weight the totals can carry. Spec-Driven PBT finds more candidate bugs on 14 of the 25 applications, fewer on 6, and the same number on 5; a two-sided sign test over the 20 applications that differ gives p = 0.12. The 126 against 113 of Table 1 is therefore not a significant difference on this cohort, and we do not claim one. The comparisons this paper rests on are the efficiency result of Appendix D.3, which holds on all 25 applications, and the complementarity of Section 6. Table 2: Per-application ViBench results, both methods, all 25 problems. Pass and fail rates use passed plus failed terminal pytest cases as the denominator, with counts in parentheses. “Underlying bugs” counts the candidate bugs the blind reviewer attributed to that suite. Table 1 gives the totals. Application collabrative kaban

Method

Spec-Driven Code-driven creative community Spec-Driven Code-driven energy audit Spec-Driven Code-driven family friendly venue Spec-Driven Code-driven family social Spec-Driven Code-driven furniture freight Spec-Driven Code-driven hvac Spec-Driven Code-driven mafia Spec-Driven Code-driven market place Spec-Driven Code-driven monopoly Spec-Driven Code-driven online whiteboard Spec-Driven Code-driven pilot logbook Spec-Driven Code-driven slack Spec-Driven Code-driven srm Spec-Driven Code-driven wedding Spec-Driven Code-driven amazon-prime Spec-Driven Code-driven

Tests

Pass rate

Fail rate Underlying bugs

23 31 15 44 29 38 52 63 21 52 16 19 24 55 13 32 16 30 13 23 12 18 23 73 27 39 26 32 9 41 26 89

39% (9) 71% (22) 33% (5) 80% (35) 52% (15) 71% (27) 88% (45) 90% (57) 76% (16) 83% (43) 31% (5) 79% (15) 65% (17) 85% (47) 54% (7) 78% (25) 81% (13) 87% (26) 69% (9) 91% (21) 25% (3) 61% (11) 74% (17) 95% (69) 78% (21) 82% (32) 50% (13) 66% (21) 22% (2) 85% (35) 50% (15) 84% (75)

61% (14) 29% (9) 67% (10) 20% (9) 48% (14) 29% (11) 12% (6) 10% (6) 24% (5) 17% (9) 69% (11) 21% (4) 35% (9) 15% (8) 46% (6) 22% (7) 19% (3) 13% (4) 31% (4) 9% (2) 75% (9) 39% (7) 26% (6) 5% (4) 22% (6) 18% (7) 50% (13) 34% (11) 78% (7) 15% (6) 50% (15) 16% (14)

19

6 5 6 4 5 6 3 2 5 4 4 2 6 5 2 3 2 2 3 2 5 4 4 3 3 3 9 10 6 5 4 5

Application

Method

Tests

asana

Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven Spec-Driven Code-driven

19 88% (44) 12% (6) 101 98% (207) 2% (5) 29 66% (19) 34% (10) 63 90% (78) 10% (9) 18 50% (9) 50% (9) 77 88% (68) 12% (9) 32 72% (23) 28% (9) 99 89% (92) 11% (11) 23 90% (70) 10% (8) 66 82% (54) 18% (12) 27 78% (21) 22% (6) 94 92% (87) 8% (8) 29 76% (22) 24% (7) 58 88% (51) 12% (7) 24 83% (20) 17% (4) 60 92% (55) 8% (5) 20 65% (13) 35% (7) 87 90% (78) 10% (9)

discord figma github google-docs instagram jira uber youtube

D.3

Pass rate

Fail rate Underlying bugs 6 3 8 7 6 6 5 6 6 5 5 5 6 4 4 4 7 8

Efficiency

Spec-Driven PBT reaches a yield of 0.22 candidate bugs per authored test against the baseline’s 0.08, a factor of 2.7. The effect is not carried by a handful of large suites: taking each application as one paired observation, Spec-Driven PBT writes fewer tests on all 25 and reaches a higher bugs-per-test ratio on all 25 (two-sided sign test, p ≈ 6 × 10−8 in both cases), with median per-application yields of 0.24 against 0.08. Figure 3 shows the per-application distribution. Bugs found against tests written One point per generation cell. Spec-Driven PBT sits up and to the left: 0.22 bugs per test at the median against 0.07

Spec-Driven PBT

Code-driven PBT

1 bug per 4 tests

10

1 per 12

candidate bugs

8

6

Spec-Driven PBT median 23 tests, 5 bugs Code-driven PBT median 55 tests, 4 bugs

4

2

0 0

20

40

60

80

100

property tests authored

Figure 3: Candidate bugs against property tests authored, one point per generation cell. Stars mark each method’s median and the dashed guides are lines of constant yield.

20

D.4

Cost and compute resources

Both methods ran on the Modal platform, one generation cell per sandbox, each a Linux/amd64 Docker container with 2 cores and 4 GiB of memory running Ubuntu 24.04. No accelerators were used: the agents reach Claude Opus 5 over the API, so what a run costs is agent wall-clock time and tokens rather than GPU hours. Both are reported below, per cell. Generation only. The pooled blind review is excluded because it runs once over both methods’ evidence and cannot be attributed to either; for the record it cost $33.06 over 1.7 hours. Table 3: Generation cost per cell on ViBench, 25 PRDs per method. Agent time (min)

Tokens (M)

Method

Mean Median Max Mean Median

Spec-Driven Code-driven

31.1 29.9

31.2 50.5 30.1 54.0

9.45 8.94

API cost ($) Max Mean Median

8.48 17.50 7.33 21.79

8.22 7.69

Max

7.83 12.82 6.60 16.47

Cost per PRD and per bug Spec-Driven PBT ran 25 cells, one per PRD, in 13.0 hours of agent time (31 min/PRD) at an API cost of $205.57 ($8.22/PRD, median $7.83, range $4.05–$12.82). It consumed 0.24 billion tokens (9.45 million/PRD) and the blind reviewer attributed 126 candidate bugs to it, so $1.63 per candidate bug and 5.0 bugs/PRD. The baseline ran 25 cells, one per PRD, in 12.4 hours of agent time (30 min/PRD) at an API cost of $192.26 ($7.69/PRD, median $6.60, range $3.43–$16.47). It consumed 0.22 billion tokens (8.94 million/PRD) and the blind reviewer attributed 113 candidate bugs to it, so $1.70 per candidate bug and 4.5 bugs/PRD. The two methods therefore cost almost the same per PRD, and Spec-Driven PBT is slightly cheaper per candidate bug because it surfaces more of them for a similar spend. Suite runtime Suite time is the wall-clock duration of each cell’s single final whole-suite pytest invocation, which is separate from agent time; Figure 4 plots one point per cell. Spec-Driven PBT’s median suite finishes 35% sooner than the baseline’s (51 s against 78 s), which follows from writing far fewer tests. The means are much closer, 3% apart (110 s against 113 s), because both distributions are dominated by a few slow suites: Spec-Driven PBT’s three slowest account for 36% of its total suite time and the baseline’s for 33%. The median is therefore the figure that describes a typical application, and the mean carries no claim on this cohort. Final suite runtime per cell Medians 51 s against 78 s (35 % lower), but means 110 s against 113 s: the tail closes the gap

Spec-Driven PBT

Code-driven PBT

median 51 s

Spec-Driven PBT

mean 110 s

median 78 s

Code-driven PBT

mean 113 s 5

10

20

50

100

200

500

seconds (log scale)

Figure 4: Final suite runtime per cell on a log scale, one point per generation cell. The solid rule is each method’s median, the dashed rule its mean.

21

Spec-only PBT (n=41) 14

Code-only PBT (n=80)

1 12

2% 2% 10

10% 12

4%

4%

1% 5%

2 Access Control 12%

5%

15

13

13

24%

Access Control 8%

9

1

Concurrency and Atomicity 6%

6%

Input Handling

35%

27%

8

10

17%

State and Lifecycle

4%

Concurrency and Atomicity 22%

Input Handling 48%

16%

6%

7

Logic and Computation

State and Lifecycle

Logic and Computation

4%

12%

27%

12%

6

3

22%

7%

11%

8

7%

5%

7%

7

12%

5

4%

4%

4

3

4

5

2

Fine-grained classes 1

Unhandled input crash

6

Component contract mismatch

11

Non-atomic operation

2

Unenforced input constraint

7

Invalid state / relationship

12

Concurrent state divergence

3

Calculation error

8

Stale derived state

13

Unauthorized access / disclosure

4

Matching / filter semantics

9

Destructive / incomplete operation

14

Identity / credential mismatch

5

Position / boundary logic

10

Check-then-act race

15

Untrusted content / paths

Figure 5: Method-exclusive candidate bugs in the controlled comparison. Inner rings show broad classes; numbered outer slices map to fine classes in the legend. Percentages are within each arm. E

Manual validation of ViBench candidate bugs

We selected a stratified pool of 50 candidate bugs across the ViBench releases and method-membership groups; the five paper case studies were excluded. Two authors assessed 25 of these cases with method labels withheld, judging bug validity. All 25 were judged to reveal genuine defects, with uncertain practical significance in four cases. For the bug taxonomy label attached to each case, the final human and LLM-applied class labels agreed on 20 of 22 broad classes (90.9%) and 17 of 21 fine-grained classes (81.0%) for which both labels were available, giving Cohen’s κ values of 0.879 for broad bug class labels and 0.784 for fine-grained bug class labels. F

Isolating specification- vs. code-grounding

To isolate the source of initial invariants, we ran matched Spec-only and Code-only agents once on each of 25 ViBench applications. They used the same model, environment, test-construction, and triage workflow. Spec-only wrote invariants from the PRD before reading code; Code-only wrote them from code without the PRD. Both then used code to implement and run tests, with prompts forbidding semantic changes to the ledger. In a tool-call audit, we found the Spec-only agents to follow this, with none of them reading the source before writing the ledger, and with each cell in both arms writing the ledger once. Failing tests were pooled by application for label-blinded LLM review. Nevertheless, it is possible that test names and assertions could suggest the method which produced the test implicitly. The reviewer mapped 258 of 268 failing-test evidence items to candidate bugs, leaving 10 unmapped. Table 4 summarizes the results. Table 4: Controlled ViBench comparison. Tests are source-level functions; bug-bearing tests and candidate bugs are attributed by the pooled LLM reviewer, not ground truth. Method

Tests Bug-bearing Bugs Unique Bugs/test

Spec-only Code-only

704 502

14.2% 31.5%

78 117

41 80

0.11 0.23

Found by both: 37 of 158 distinct candidates (Jaccard 23.4%)

We applied the paper’s taxonomy to all 158 candidates. Two labeling passes agreed on 154 broad and 154 fine-grained labels (97.5% each); Figure 5 uses the first. 22

G

Stochasticity across Repeated Agent Runs

We examined three runs per method on the same 25 ViBench applications, pooling all six suites per application in one LLM review. Run 0 reuses the submitted suites; its candidate counts differ from Table 1 because they were reviewed in this larger pool. We applied the paper’s taxonomy to the 270 distinct candidates. Table 5 gives counts by run and Figure 6 shows their class distributions. Table 5: Tests, reviewer-attributed candidate bugs, and class counts across three runs per method. Class entries give counts (share of that run’s candidate bugs); state/concurrency combines state, lifecycle, data integrity, concurrency, and atomicity. Method

H

Run Tests Candidate bugs Input handling State/concurrency

Spec-Driven 0 1 2

566 519 538

131 115 123

36 (27%) 30 (26%) 32 (26%)

38 (29%) 35 (30%) 38 (31%)

Code-driven 0 1 2

1384 1417 1339

118 130 131

49 (42%) 61 (47%) 63 (48%)

23 (19%) 20 (15%) 22 (17%)

Qualitative bug taxonomy

The taxonomy was induced from all 169 canonical ViBench candidate-bug reports. Each candidate receives exactly one of the fifteen fine-grained labels nested under five broad categories. The hierarchy and definitions are presented together below. Following the ViBench qualitative-analysis protocol [Zhong et al., 2026], we supplied an LLM-driven agent with all candidate bugs and asked it to induce at most five broad and fifteen fine-grained fault classes. A separate Claude Opus 5 agent then applied this taxonomy twice to the method-exclusive bugs, with method labels withheld at both stages. The two classification passes agreed on 98% of broad and 97% of fine-grained labels. H.1

Taxonomy and definitions

Input Handling and Robustness. The application accepts a value from a client, a URL, a file upload or its own configuration and then uses it without checking that it is usable. Either the request dies in a lower layer, or an unacceptable value is taken in and used as if it were valid. Unhandled input reaches a lower layer. A supplied value the code cannot process propagates into the database driver, a parser, arithmetic or an absent API and aborts the operation, instead of being answered with the ordinary client-error the same endpoint already produces for comparable input. Declared input constraint not enforced. A limit or allowed-value rule that the product states, or that another entry point already applies, is missing, applied on only some paths, or defeated by type coercion, so an out-of-domain value is accepted and used. Domain Logic, Computation and Internal Contracts. The application runs its own rules and produces the wrong answer: a wrong number, a wrong result set, a wrong position in a document or list, or a value that one component writes and another misreads. Wrong computed or aggregated value. A formula, allocation or aggregation is implemented incorrectly, so the number the application reports or stores is not the one its own rules define. Wrong search, filter, or lookup result. A search, filter or record lookup returns items it should not, or omits items it should return, because the matching rule does not mean what the product says it means. Wrong position, boundary, or interval. Positions, ranges, addresses or geometry are derived or interpreted incorrectly, so content lands in the wrong place, is cut in the wrong place, or is not reachable at all. 23

Spec-Driven PBT, run 0 (n=131)

15 14

4%

3%

13

5%

1

5%

Access Control 14%

1% 2%

10

Input Handling

1 36%

3%

27%

10

5%

12 11

Access Control 16%

1% 2%

4%

13

22%

9% 12 11

Code-driven PBT, run 0 (n=118)

15

14

9

Concurrency 7%

Concurrency 5%

3%

Input Handling 42%

8

State and Lifecycle

3%

14%

State and Lifecycle

Logic and Computation

22%

7%

8

2

5%

5%

9

6%

8%

7

3

Logic and Computation

27%

25%

6% 11%

10% 7

4%

6%

6

5

6%

6 5%

4 5

12

13 15%

6%

26%

11%

8

2

3%

Input Handling

13%

47%

6%

22%

7%

Logic and Computation

3

9%

25%

5%

12%

7 6%

Logic and Computation

7%

6

31%

5 4

6%

8%

3

Code-driven PBT, run 2 (n=131)

15

14

15 14 1

3% 2%

13 11

19%

11%

10

12

Access Control 15%

1% 2%

7%

5%

9

Concurrency 10%

7%

2

Access Control 12%

Concurrency 5%

5%

8

3%

7

5%

4%

4% 1%

4%

Input Handling 26%

10

38%

State and Lifecycle

State and Lifecycle

Logic and Computation

21%

7%

7%

48%

6

5% 6

23%

5

4

11%

5% 3%

9%

7

Logic and Computation

3

28%

8

1

Input Handling

12%

4%

9

6% 2

5

Spec-Driven PBT, run 2 (n=123)

13

5%

4

6

11

1

41%

State and Lifecycle

State and Lifecycle

10%

8

Access Control 12%

Concurrency 2%

3% 7

3%

5%

4%

Input Handling Concurrency 9%

5%

1% 2%

9

8%

9

11 10

Access Control 12%

10

15

14

1

2%

4%

1%

Code-driven PBT, run 1 (n=130)

15

14

3

4

Spec-Driven PBT, run 1 (n=115)

13

2

6%

8%

10%

7%

10% 5%

4

2

5

3

Fine-grained classes 1

Unhandled input crash

6

Component contract mismatch

11

Non-atomic operation

2

Unenforced input constraint

7

Invalid state / relationship

12

Concurrent state divergence

3

Calculation error

8

Stale derived state

13

Unauthorized access / disclosure

4

Matching / filter semantics

9

Destructive / incomplete operation

14

Identity / credential mismatch

5

Position / boundary logic

10

Check-then-act race

15

Untrusted content / paths

Figure 6: Bug-class composition across three runs per method, using the same sunburst styling and taxonomy as Figure 2. “Concurrency” abbreviates “Concurrency and Atomicity” inside the smaller plots. Numbered outer slices map to fine classes in the shared legend. A candidate appearing in multiple runs is counted in each of those runs.

24

Component contract mismatch. One part of the system writes, names, encodes or advertises something in a way another part does not expect, so the two behave as if they were built against different specifications. State, Lifecycle and Data Integrity. Persisted records end up in a shape the product forbids, keep values that a later change invalidated, or lose data because an operation cleaned up, cascaded or reversed itself incorrectly. Illegal state, transition, or relationship. An operation moves an object into a status, or creates a link between objects, that the product’s own rules say cannot exist - usually because the current state or the surrounding relationships were never re-checked. Derived state not refreshed. Something computed or cached from other data - a result, a flag, a snapshot, a pending record or a displayed indicator - keeps its old value after the data it was derived from changed. Destructive or incomplete operation. An operation deletes or overwrites more than it should, leaves related records unusable, or records an inverse that cannot faithfully restore what was there before. Concurrency and Atomicity. The defect appears only when two operations overlap, interleave, or when one operation fails part-way through. A single sequential run behaves correctly. Unsynchronized check-then-write. A limit, uniqueness rule or counter is verified by a read and then applied by a separate write, with no lock or constraint tying the two together, so overlapping requests all pass the check. Partial effects from a non-atomic operation. A multi-step operation is not wrapped as a unit, so a rejection or error part-way through leaves some steps applied and the caller told the operation did not happen. Concurrent state divergence. Two or more participants acting at the same time end up with different views of shared state, or one participant’s update silently absorbs or discards another’s, even though every individual request succeeded. Access Control, Identity and Untrusted Content. Content or capability reaches a party that should not have it, an account cannot be identified consistently, or untrusted input is emitted or resolved without being neutralised. Missing or inconsistent access control. An endpoint, field or embedded object is served or mutated without the visibility, ownership or role check that the rest of the application applies to the same data. Identity or credential mismatch. The value used to identify an account is stored, compared or generated inconsistently, so accounts become unreachable, duplicated, or blocked by a name collision. Untrusted content or unsafe path. User-supplied text, files or URLs are interpolated into markup, served with an attacker-chosen content type, followed as a redirect target, or joined onto a filesystem path without being neutralised or confined. H.2

Results

Table 6: Distribution of method-exclusive ViBench candidate bugs across the five broad categories. Broad category

Spec-Driven only (n = 56) Code-driven only (n = 43)

Input Handling and Robustness Domain Logic, Computation and Internal Contracts State, Lifecycle and Data Integrity Concurrency and Atomicity Access Control, Identity and Untrusted Content

9 (16.1%) 15 (26.8%) 19 (33.9%) 7 (12.5%) 6 (10.7%)

25

21 (48.8%) 8 (18.6%) 5 (11.6%) 4 (9.3%) 5 (11.6%)

I

Bug Reports

The agents’ own reports for the five bugs shared as case studies in Section 6. Each was written by the agent at the end of its run. I.1

Found only by Spec-Driven PBT: a follow of a public account stays pending # Bug Report: following a public account stays stuck at "pending" when a stale follow request exists **Target**: ‘server/routers/follows.py::follow‘ **Severity**: Medium **Bug Type**: Logic **Date**: 2026-09-09 ## Summary ‘follow‘ returns early on *any* existing ‘follows‘ row: ‘if existing: return {"status": existing["status"]}‘. A pending request created while the target was private therefore survives the target switching to public, and every later follow attempt keeps answering ‘pending‘. The follower can never follow the now-public account (the UI shows "Requested"), and the account’s posts never reach their home feed, until the requester happens to cancel the request first. ## Property-Based Test ‘‘‘python PRIORS = ["none", "already_following", "unfollowed", "request_declined_while_private", "request_pending_from_private_days", "blocked_then_unblocked"]

@given(prior=st.sampled_from(PRIORS)) @settings(max_examples=len(PRIORS) * 3, deadline=None, suppress_health_check=[HealthCheck.too_slow]) def test_following_a_public_account_takes_effect_immediately(prior): """PRD: "Following a public account takes effect immediately." """ target = make_user("public") viewer = make_user("public") post = target.create_post(caption="hello from a public account") _reach_state(viewer, target, prior) assert target.get(f"/users/{target.username}").json()["user"]["visibility"] == "public" r = viewer.follow(target) assert r.status_code == 200, r.text assert r.json()["status"] == "accepted", ( f"prior={prior}: following a public account returned {r.json()[’status’]!r}" ) rel = viewer.relationship_to(target) assert rel["following"] is True and rel["requested"] is False, (prior, rel) feed_ids = [p["id"] for p in viewer.get("/feed").json()["posts"]] assert post["id"] in feed_ids, f"prior={prior}: followed post missing from the home feed" ‘‘‘ where the failing prior state is reached by ‘‘‘python elif prior == "request_pending_from_private_days": target.set_visibility("private") viewer.follow(target) target.set_visibility("public") ‘‘‘ **Failing input**: ‘prior=’request_pending_from_private_days’‘ --‘AssertionError: following a public account returned ’pending’‘. ## Reproducing the Bug ‘‘‘python import requests, uuid API = "http://localhost:8000/api" def signup(visibility="public"): name = "u" + uuid.uuid4().hex[:10] r = requests.post(f"{API}/auth/signup", json={ "username": name, "email": f"{name}@example.com", "display_name": name, "password": "password123", "visibility": visibility}) return name, {"Authorization": "Bearer " + r.json()["token"]}

26

target, th = signup("private") viewer, vh = signup() assert requests.post(f"{API}/users/{target}/follow", headers=vh).json()["status"] == "pending" requests.patch(f"{API}/me", json={"visibility": "public"}, headers=th) r = requests.post(f"{API}/users/{target}/follow", headers=vh) print(r.json()) rel = requests.get(f"{API}/users/{target}", headers=vh).json()["user"]["relationship"] print(rel) assert r.json()["status"] == "accepted", "public follow did not take effect" ‘‘‘ Output: ‘‘‘ {’status’: ’pending’} {’is_self’: False, ’following’: False, ’requested’: True, ...} ‘‘‘ ## Why This Is A Bug The PRD states plainly: "Following a **public** account takes effect immediately. Following a **private** account creates a pending **follow request** the owner must approve or decline". Pending requests only exist for private accounts, so once the target is public a follow must produce an accepted edge. Instead the account is unfollowable through the normal path, its posts are silently missing from the follower’s reverse-chronological home feed (the profile shows them, the feed does not), and the now-public owner is left holding an approval queue the PRD never describes for a public account. ## Fix Only honour an existing row when it is already accepted, or when the target is still private; otherwise promote the stale request. ‘‘‘diff --- a/server/routers/follows.py +++ b/server/routers/follows.py @@ existing = query_one( "SELECT * FROM follows WHERE follower_id = %s AND followee_id = %s", (user["id"], target["id"]) ) if existing: return {"status": existing["status"]} status = "accepted" if target["visibility"] == "public" else "pending" + if existing: + if existing["status"] == "accepted" or status == "pending": + return {"status": existing["status"]} + execute( + "UPDATE follows SET status = ’accepted’ WHERE follower_id = %s AND followee_id = %s", + (user["id"], target["id"]), + ) + return {"status": "accepted"} execute( "INSERT INTO follows (follower_id, followee_id, status) VALUES (%s,%s,%s) ON CONFLICT DO NOTHING", (user["id"], target["id"], status), ) return {"status": status} ‘‘‘ (Converting outstanding requests at the moment the account switches to public, in ‘users.update_profile‘, would additionally clear the stale approval queue.)

I.2

Found only by Spec-Driven PBT: accepted commits are silently lost # Bug Report: backend.routes_git.make_commit Loses Commits and Silently Discards Merges (Missing Branch Lock) **Target**: ‘backend/routes_git.py::make_commit‘ (‘POST /api/repos/{owner}/{name}/commits‘) **Severity**: High **Bug Type**: Logic **Date**: 2026-09-09

27

## Summary ‘make_commit‘ reads ‘branch.head_id‘, builds the new tree from it, and writes ‘branch.head_id‘ back without taking a row lock on the branch --- unlike ‘cherry_pick‘, ‘revert‘ and ‘merge_pull‘, which all use ‘select(Branch)...with_for_update()‘. Concurrent writes to one branch therefore lost-update each other: every request returns ‘201 Created‘ but only the last writer’s commit stays on the branch. When a plain commit races a pull-request merge on the same branch, the merge is the one that gets discarded: the PR is left in state ‘merged‘ with a ‘merge_commit_id‘ that is not in the base branch’s history, the head branch’s changes never reach the base, and the PR cannot be reopened. ## Property-Based Test ‘‘‘python @CONC @given(payload=st.text(alphabet="abcdef", min_size=1, max_size=6)) def test_merged_pull_request_always_reaches_its_base_branch(make_user, payload): owner = make_user() reviewer = make_user() repo = owner.new_repo() owner.post( f"/api/repos/{repo}/collaborators", {"username": reviewer.username, "role": "write"}, ) owner.commit( repo, "main", "init", [{"path": "base.txt", "action": "create", "content": "1\n"}] ) owner.post(f"/api/repos/{repo}/branches", {"name": "feature", "source": "main"}) owner.commit( repo, "feature", "feature work", [{"path": "feature.txt", "action": "create", "content": payload + "\n"}], ) pr = owner.post( f"/api/repos/{repo}/pulls", {"title": "p", "head": "feature", "base": "main"} ) number = pr["number"] reviewer.post(f"/api/repos/{repo}/pulls/{number}/reviews", {"state": "approve"}) def do_merge(): c = _sibling(owner) try: return c.req("POST", f"/api/repos/{repo}/pulls/{number}/merge") finally: c.close() def do_commit(): c = _sibling(owner) try: return c.req( "POST", f"/api/repos/{repo}/commits", json={ "branch": "main", "message": "unrelated direct commit", "changes": [ {"path": "direct.txt", "action": "create", "content": "d\n"} ], }, ) finally: c.close() merge_res, _commit_res = _run_parallel([do_merge, do_commit]) pr_state = owner.get(f"/api/repos/{repo}/pulls/{number}") history = [ c["id"] for c in owner.get(f"/api/repos/{repo}/commits", params={"ref": "main"})["commits"] ] tree = owner.tree(repo, "main") if merge_res.status_code < 400: assert pr_state["state"] == "merged" assert pr_state["merge_commit_id"] in history assert "feature.txt" in tree else: assert pr_state["state"] == "open", pr_state["state"]

28

‘‘‘ **Failing input**: ‘payload=’a’‘ --- any value fails; the minimal shrink of the commit-only variant is ‘n_writers=2‘. ## Reproducing the Bug ‘‘‘python import concurrent.futures as cf import httpx BASE = "http://localhost:8000"

def signup(username): c = httpx.Client(base_url=BASE, timeout=60) c.post( "/api/auth/signup", json={ "name": username, "username": username, "email": f"{username}@example.com", "password": "pw123456", }, ) return c

owner = signup("race-owner") reviewer = signup("race-reviewer") repo = "race-owner/race-repo" owner.post("/api/repos", json={"name": "race-repo", "visibility": "public"}) owner.post( f"/api/repos/{repo}/collaborators", json={"username": "race-reviewer", "role": "write"} ) owner.post( f"/api/repos/{repo}/commits", json={ "branch": "main", "message": "init", "changes": [{"path": "base.txt", "action": "create", "content": "1\n"}], }, ) owner.post(f"/api/repos/{repo}/branches", json={"name": "feature", "source": "main"}) owner.post( f"/api/repos/{repo}/commits", json={ "branch": "feature", "message": "feature work", "changes": [{"path": "feature.txt", "action": "create", "content": "f\n"}], }, ) n = owner.post( f"/api/repos/{repo}/pulls", json={"title": "p", "head": "feature", "base": "main"} ).json()["number"] reviewer.post(f"/api/repos/{repo}/pulls/{n}/reviews", json={"state": "approve"})

def merge(): c = httpx.Client(base_url=BASE, cookies=owner.cookies, timeout=60) return c.post(f"/api/repos/{repo}/pulls/{n}/merge")

def commit(): c = httpx.Client(base_url=BASE, cookies=owner.cookies, timeout=60) return c.post( f"/api/repos/{repo}/commits", json={ "branch": "main", "message": "direct", "changes": [{"path": "direct.txt", "action": "create", "content": "d\n"}], }, )

with cf.ThreadPoolExecutor(max_workers=2) as pool: f1, f2 = pool.submit(merge), pool.submit(commit) r_merge, r_commit = f1.result(), f2.result()

29

pr = owner.get(f"/api/repos/{repo}/pulls/{n}").json() history = [ c["id"] for c in owner.get(f"/api/repos/{repo}/commits", params={"ref": "main"}).json()["commits"] ] paths = owner.get(f"/api/repos/{repo}/tree", params={"ref": "main"}).json()["all_paths"] print("merge:", r_merge.status_code, "commit:", r_commit.status_code) print("pr state:", pr["state"], "merge commit in history:", pr["merge_commit_id"] in history) print("main tree:", paths) print("reopen:", owner.post(f"/api/repos/{repo}/pulls/{n}/reopen").status_code) ‘‘‘ Output: ‘‘‘ merge: 200 commit: 201 pr state: merged merge commit in history: False main tree: [’base.txt’, ’direct.txt’] reopen: 400 ‘‘‘ ## Why This Is A Bug The PRD states that "A commit advances the branch’s tip and updates its tree accordingly", that "History is append-only", and --- for merges specifically --that "Merge-gate evaluation and the merge’s application are atomic against the base as it stands at that moment: when two merges race for the same base, the first to commit takes effect, and any competing merge is re-evaluated against the advanced base." Here neither holds. Both requests read the same ‘head_id‘, each creates a commit parented on it, and the second ‘UPDATE branches SET head_id‘ overwrites the first. The overwritten commit is orphaned: it exists as a row but is not reachable from any branch, so its changes vanish while the API reported success. In the merge case the result is worse than a lost commit --- the PR’s recorded state (‘merged‘, plus a ‘merge_commit_id‘) contradicts the repository, ‘feature.txt‘ is absent from ‘main‘, and "A merged pull request cannot be reopened" makes the state unrecoverable through the API. That ‘cherry_pick‘, ‘revert‘ and ‘merge_pull‘ all lock the branch row while ‘make_commit‘ does not shows this is an omission rather than a design choice; the merge/merge race is in fact handled correctly (verified separately: one merge wins, the other gets 409). ## Fix Lock the branch row before reading its tip, matching the other write paths. ‘‘‘diff --- a/backend/routes_git.py +++ b/backend/routes_git.py @@ -277,9 +277,14 @@ def make_commit( ): repo = get_repo(db, owner, name, user) require_write(db, repo, user) branch = get_branch(db, repo.id, payload.branch) + branch = db.execute( + select(Branch) + .where(Branch.repo_id == repo.id, Branch.name == payload.branch) + .with_for_update() + ).scalar_one_or_none() if branch is None: raise HTTPException(status_code=404, detail="Branch not found") + db.refresh(branch) message = (payload.message or "").strip() if not message: raise HTTPException(status_code=400, detail="A commit message is required") ‘‘‘

I.3

Found only by Code-driven PBT: a malformed quantity crashes the cart # Bug Report: Unparseable numeric fields return HTTP 500 instead of the documented 4xx error codes **Target**: ‘routes_seller._validate_listing‘, ‘routes_shop.add_to_cart‘, ‘mutations.place_order‘, ‘auth.validate_name‘ **Severity**: Medium

30

**Bug Type**: Crash **Date**: 2026-09-04 ## Summary The write routes validate their numeric inputs inconsistently: ‘stock‘, ‘rating‘ and ‘dealQuantity‘ are wrapped in ‘try/except (TypeError, ValueError)‘ and answer with a ‘400‘ and a stable error code, while the adjacent ‘price‘ / ‘priceCents‘ / ‘qty‘ / ‘expectedTotalCents‘ fields call ‘int()‘ or ‘money.to_cents()‘ bare. A blank or non-numeric value there escapes as an unhandled exception and is turned into a ‘500 SERVER_ERROR‘ by ‘main.unhandled_handler‘, whose response also echoes the raw exception text (‘"message": str(exc)‘). ## Property-Based Test ‘‘‘python bad_money = st.sampled_from(["", "abc", "$19.99", "19,99", "nan", "1.2.3", " "])

@given(price=bad_money) def test_unparseable_listing_price_is_a_client_error(api, seller, price): status, body = api.call( "POST", "/api/seller/listings", {"title": uniq("t-"), "category": "General", "price": price, "stock": 1}, seller["token"], ) assert status == 400, body assert body["code"] == "INVALID_PRICE" ‘‘‘ **Failing input**: ‘price=""‘ (an empty price field) -> ‘500‘, ‘{"code": "SERVER_ERROR", "message": "[<class ’decimal.ConversionSyntax’>]"}‘. The sibling test ‘test_unparseable_listing_stock_is_a_client_error‘ passes with the same kind of input, which is what pins the intended contract. ## Reproducing the Bug ‘‘‘python import json, urllib.error, urllib.request, uuid BASE = "http://127.0.0.1:8000"

def call(method, path, body=None, token=None): req = urllib.request.Request(BASE + path, data=json.dumps(body).encode(), method=method) req.add_header("content-type", "application/json") if token: req.add_header("authorization", "Bearer " + token) try: with urllib.request.urlopen(req) as resp: return resp.status, json.loads(resp.read()) except urllib.error.HTTPError as exc: return exc.code, json.loads(exc.read())

tag = uuid.uuid4().hex[:8] _, seller = call("POST", "/api/auth/signup", { "name": "s", "email": f"s{tag}@example.test", "password": "hunter2pw", "role": "seller", "storeName": f"store-{tag}"}) token = seller["token"] _, shopper = call("POST", "/api/auth/signup", { "name": "b", "email": f"b{tag}@example.test", "password": "hunter2pw", "role": "shopper"}) print(call("POST", "/api/seller/listings", {"title": "t", "category": "General", "price": "", "stock": 1}, token)[0]) print(call("POST", "/api/seller/listings", {"title": "t", "category": "General", "priceCents": "1.5", "stock": 1}, token)[0]) print(call("POST", "/api/seller/listings", {"title": "t", "category": "General", "priceCents": 500, "stock": "abc"}, token)[0]) print(call("POST", "/api/auth/signup", {"name": 123, "email": f"n{tag}@example.test", "password": "hunter2pw", "role": "shopper"})[0]) ‘‘‘ ‘‘‘ 500 500 400 500 ‘‘‘

<- POST /api/seller/listings price: "" <- POST /api/seller/listings priceCents: "1.5" <- POST /api/seller/listings stock: "abc" (handled, for contrast) <- POST /api/auth/signup name: 123

31

Also reproducing as ‘500‘: | Request | Field | Code path | | --- | --- | --- | | ‘POST /api/cart‘ | ‘qty: "1.5"‘ | ‘routes_shop.add_to_cart‘ -> ‘int(...)‘ | | ‘PATCH /api/cart/{id}‘ | ‘qty: "abc"‘ | ‘routes_shop.update_cart_item‘ -> ‘int(...)‘ | | ‘POST /api/orders‘ | ‘expectedTotalCents: "abc"‘ | ‘mutations.place_order‘ -> ‘int(...)‘ | | ‘POST /api/auth/signup‘ | ‘name: 123‘ | ‘auth.validate_name‘ -> ‘(name or "").strip()‘ | ## Why This Is A Bug * ‘services.err‘ and the ‘HTTPException‘ handler define the API contract: a ‘{code, message}‘ body with a 4xx status. ‘_validate_listing‘ already produces ‘INVALID_PRICE‘ for a non-positive price and ‘INVALID_STOCK‘ for an unparseable stock --- the price branch simply lacks the same guard, three lines above the one that has it. * ‘auth.validate_password‘ explicitly rejects non-string input (‘if password is None or not isinstance(password, str)‘), so type-safety on ‘validate_name‘ is clearly intended too. * An empty string is what an HTML form submits for a field the seller left blank, so this is ordinary user input, not a synthetic edge case: the seller sees "Unexpected server error" instead of "Enter a price greater than $0.00." * The 500 body also leaks internals (‘str(exc)‘ includes the failing SQL statement or ‘decimal.ConversionSyntax‘). ## Fix Give the numeric fields the same guard the neighbouring ones already have. ‘‘‘diff --- a/backend/routes_seller.py +++ b/backend/routes_seller.py @@ def _validate_listing(payload: dict, partial: bool = False) -> dict: if "price" in payload or "priceCents" in payload or not partial: cents = int(payload["priceCents"]) if payload.get("priceCents") is not None else to_cents(payload.get("price")) + try: + cents = ( + int(payload["priceCents"]) + if payload.get("priceCents") is not None + else to_cents(payload.get("price")) + ) + except (TypeError, ValueError, ArithmeticError): + raise err(400, "INVALID_PRICE", "Enter a price greater than $0.00.") if cents <= 0: raise err(400, "INVALID_PRICE", "Enter a price greater than $0.00.") out["price_cents"] = cents --- a/backend/routes_shop.py +++ b/backend/routes_shop.py @@ def add_to_cart(payload: dict = Body(...), db: Session = Depends(get_db), user: User = Depends(require_shopper)): qty = int(payload.get("qty") or 1) + try: + qty = int(payload.get("qty") or 1) + except (TypeError, ValueError): + raise err(400, "INVALID_QTY", "Quantity must be at least 1.") if qty <= 0: raise err(400, "INVALID_QTY", "Quantity must be at least 1.") --- a/backend/auth.py +++ b/backend/auth.py @@ def validate_name(name: str) -> str: n = (name or "").strip() + if name is not None and not isinstance(name, str): + raise HTTPException( + status_code=400, + detail={"code": "INVALID_NAME", "message": "Name must be 1-80 characters and cannot be only whitespace."}, + ) + n = (name or "").strip() ‘‘‘ The same treatment is needed for ‘update_cart_item‘’s ‘qty‘, ‘place_order‘’s ‘expectedTotalCents‘, and the variant/deal price parsing in ‘routes_seller‘ (‘create_listing‘, ‘update_listing‘, ‘create_deal‘).

32

I.4

Found only by Code-driven PBT: a username is stored under a different string # Bug Report: ‘core.views.register_view‘ stores a different username than the one validated (NFKC) **Target**: ‘core.views.register_view‘ / ‘core.forms.RegistrationForm.clean_username‘ **Severity**: Medium **Bug Type**: Logic (with a Crash symptom) **Date**: 2026-09-09 ## Summary ‘RegistrationForm.clean_username‘ checks availability of the *raw* username, but ‘User.objects.create_user()‘ stores the NFKC-normalised form of it. For any username that is not NFKC-stable (e.g. ‘’<U+00AA>’‘, ‘’<U+FB00>’‘, full-width ‘’<U+FF21>’‘) the account is created under a different name, so the member can never log in again; and if the normalised name is already taken the uniqueness check is bypassed and the view dies with an ‘IntegrityError‘ (HTTP 500). ## Property-Based Test ‘‘‘python @given(username=unicode_usernames, email=emails, password=passwords) def test_credentials_used_to_register_can_be_used_to_log_in(self, username, email, password): code = make_invite_code() self.client.post(’/register/’, registration_payload(username, email, password, code.code)) self.client.get(’/logout/’) response = self.client.post(’/login/’, {’username’: username, ’password’: password}) self.assertEqual(response.status_code, 302, f’cannot log in as {username!r} right after registering with it’)

@given(username=unicode_usernames, password=passwords) def test_second_registration_with_same_username_is_rejected(self, username, password): """"Username already taken." -- the same username never registers twice.""" code = make_invite_code() first = self.client.post( ’/register/’, registration_payload(username, ’first@example.com’, password, code.code)) assume(first.status_code == 302) self.client.get(’/logout/’) second = self.client.post( ’/register/’, registration_payload(username, ’second@example.com’, password, code.code)) self.assertEqual(second.status_code, 200, ’duplicate username was not rejected cleanly’) self.assertEqual(User.objects.count(), 1) ‘‘‘ **Failing input**: ‘username=’<U+00AA>’‘ (NFKC-normalises to ‘’a’‘) ## Reproducing the Bug ‘‘‘python import os os.environ[’DJANGO_SETTINGS_MODULE’] = ’creative_community.settings’ os.environ[’POSTGRES_DATABASE_URL’] = ’postgres://postgres:postgres@127.0.0.1:5432/creative_community’ import django django.setup() from django.contrib.auth.models import User from django.test import Client from core.models import InviteCode InviteCode.objects.get_or_create( code=’REPRO’, defaults={’code_type’: ’multi’, ’max_uses’: 100} ) client = Client() client.post(’/register/’, { ’username’: ’<U+00AA>’, ’email’: ’one@example.com’, ’password’: ’pw’, ’password_confirm’: ’pw’, ’invite_code’: ’REPRO’, }) print(list(User.objects.values_list(’username’, flat=True))) # [’a’] -- not ’<U+00AA>’ client.get(’/logout/’)

33

print(client.post(’/login/’, {’username’: ’<U+00AA>’, ’password’: ’pw’}).status_code) # 200 = login failed client.post(’/register/’, { ’username’: ’<U+00AA>’, ’email’: ’two@example.com’, ’password’: ’pw’, ’password_confirm’: ’pw’, ’invite_code’: ’REPRO’, }) # django.db.utils.IntegrityError: duplicate key value ... (username)=(a) ‘‘‘ ## Why This Is A Bug ‘clean_username‘ promises "Username already taken." for names that are in use, and the account the view creates is expected to be the one the visitor typed: ‘register_view‘ logs them in immediately, so the *only* later route into the account is ‘login_view‘, which looks the username up verbatim (‘ModelBackend‘ -> ‘get_by_natural_key‘). Two concrete consequences: 1. **Silent lockout** -- registering as ‘’<U+00AA>’‘ creates the user ‘’a’‘; the invite code is consumed and the member is locked out as soon as the session ends. 2. **Unhandled 500** -- when the normalised name already exists, the uniqueness check misses it and the ‘create_user()‘ call violates the ‘auth_user_username_key‘ constraint. ‘MemberProfile‘/‘InviteCodeUsage‘ are not created but ‘InviteCode.current_uses‘ has not been touched yet, so the state is merely wasted, not corrupted. Django’s own ‘UserCreationForm‘ avoids this by normalising the username in ‘clean_username‘; this hand-written form does not. ## Fix Normalise the username in the form so that validation and storage agree: ‘‘‘diff --- a/core/forms.py +++ b/core/forms.py @@ from django import forms from django.contrib.auth.models import User from .models import MemberProfile, InviteCode, Event @@ def clean_username(self): username = self.cleaned_data[’username’] + username = User.normalize_username(self.cleaned_data[’username’]) + if len(username) > 150: + raise forms.ValidationError(’Username is too long.’) if User.objects.filter(username=username).exists(): raise forms.ValidationError(’Username already taken.’) return username ‘‘‘

I.5

Found by both methods: the kick rule is written twice and the copies disagree # Bug Report: Discord ‘can_be_kicked‘ contradicts the kick endpoint for equal-ranked members **Target**: ‘server/routes.js‘ (‘serverSnapshot‘’s ‘can_be_kicked‘ vs ‘DELETE /api/servers/:serverId/members/:userId‘) **Severity**: Low **Bug Type**: Contract **Date**: 2026-09-09 ## Summary The kick endpoint refuses only when the target’s highest role position is **strictly greater** than the actor’s (‘rank > myRank‘), matching the PRD’s "outranks". The server snapshot advertises the same capability with ‘rank < myRank‘, so for two members of equal rank --- e.g. two members holding only ‘@everyone‘, the most common case in a small server --- the snapshot reports ‘can_be_kicked: false‘ while the endpoint happily performs the kick. The UI hides the kick control for an action the API permits. ## Property-Based Test ‘‘‘python ranks = st.sampled_from([None, 1, 2, 3])

@settings(max_examples=20, deadline=None, suppress_health_check=[HealthCheck.function_scoped_fixture]) @given(actor_rank=ranks, target_rank=ranks)

34

def test_can_be_kicked_matches_the_prd_and_the_endpoint(guild, actor_rank, target_rank): owner, actor, target, sid = guild["owner"], guild["actor"], guild["target"], guild["sid"] for client, rank in ((actor, actor_rank), (target, target_rank)): try: join(client, guild["code"]) except Exception: pass for pos, rid in guild["roles"].items(): path = f"/api/servers/{sid}/members/{client.user[’id’]}/roles/{rid}" owner.call("PUT", path) if rank == pos else owner.call("DELETE", path) snap = actor.snapshot(sid) me = [m for m in snap["members"] if m["user_id"] == actor.user["id"]][0] them = [m for m in snap["members"] if m["user_id"] == target.user["id"]][0] # PRD: the actor may kick unless the target’s highest role *outranks* the actor’s. prd_allows = (them["highest_position"] or 0) <= (me["highest_position"] or 0) resp = actor.req("DELETE", f"/api/servers/{sid}/members/{target.user[’id’]}") kicked = resp.status_code == 200 assert kicked == prd_allows assert them["can_be_kicked"] == kicked, ( f"snapshot advertised can_be_kicked={them[’can_be_kicked’]} for a member with rank " f"{them[’highest_position’]} (actor rank {me[’highest_position’]}), but the kick " f"{’succeeded’ if kicked else ’failed’}" ) ‘‘‘ **Failing input**: ‘actor_rank=None, target_rank=None‘ (both members hold only ‘@everyone‘) -> ‘snapshot advertised can_be_kicked=False for a member with rank 0 (actor rank 0), but the kick succeeded‘. ## Reproducing the Bug ‘‘‘python import uuid, requests BASE = "http://localhost:8000"

def signup(display_name): s = requests.Session() u = "u" + uuid.uuid4().hex[:12] s.post(f"{BASE}/api/auth/signup", json={"username": u, "email": f"{u}@example.com", "password": "pw-test-1234", "display_name": display_name}).raise_for_status() return s

def call(s, method, path, **kw): r = s.request(method, BASE + path, **kw) r.raise_for_status() return r.json()

owner, actor, target = signup("Owner"), signup("Actor"), signup("Target") srv = call(owner, "POST", "/api/servers", json={"name": "k-" + uuid.uuid4().hex[:6]})["server"] sid, code = srv["server"]["id"], srv["server"]["invite_code"] everyone = [r for r in srv["roles"] if r["is_everyone"]][0]["id"] call(actor, "POST", "/api/servers/join", json={"code": code}) call(target, "POST", "/api/servers/join", json={"code": code}) call(owner, "PATCH", f"/api/roles/{everyone}", json={"permissions": ["view_channel", "send_messages", "kick_members"]}) snap = call(actor, "GET", f"/api/servers/{sid}")["server"] them = [m for m in snap["members"] if m["display_name"] == "Target"][0] print("advertised:", {k: them[k] for k in ("highest_position", "can_be_kicked")}) r = actor.delete(f"{BASE}/api/servers/{sid}/members/{them[’user_id’]}") print("actual kick:", r.status_code, r.text) print("members now:", [m["display_name"] for m in call(owner, "GET", f"/api/servers/{sid}")["server"]["members"]]) ‘‘‘ Output: ‘‘‘ advertised: {’highest_position’: 0, ’can_be_kicked’: False} actual kick: 200 {"ok":true} members now: [’Actor’, ’Owner’] ‘‘‘

35

## Why This Is A Bug The PRD says a member with the kick permission "can remove another member (but not the owner, and not someone whose highest role outranks the actor’s)" --- an equal rank does not outrank, so the endpoint’s behaviour is the correct one and ‘can_be_kicked‘ is the field that is wrong. The snapshot is the only source a client has for rendering the kick affordance (‘Shell.jsx‘ drives the member-list kick button off it), so a permitted moderation action is unavailable in the product while remaining available to anyone calling the API directly. The two predicates must be derived from one rule. ## Fix ‘‘‘diff --- a/server/routes.js +++ b/server/routes.js @@ async function serverSnapshot(serverId, userId) { can_be_kicked: canKick && ctx.server.owner_id !== m.user_id && m.user_id !== userId && rank < myRank, + // Matches DELETE /servers/:serverId/members/:userId : refuse only if the target outranks the actor. + can_be_kicked: canKick && ctx.server.owner_id !== m.user_id && m.user_id !== userId && rank <= myRank, ‘‘‘

36

NeurIPS Paper Checklist 1. Claims Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope? Answer: [Yes] Justification: The abstract and the contribution bullets in Section 1 state the headline results — 2.4× fewer tests and 169 distinct bugs of which nearly 60% are found by only one method — together with the qualitative claim about which bug classes each method surfaces. These are supported by Table 1 and Figure 2, and the scope is confined to the two testbeds described in Section 4. Guidelines: • The answer [N/A] means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A [No] or [N/A] answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 2. Limitations Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [Yes] Justification: Section 7 discusses the absence of ground-truth bug labels on ViBench, the limits of validation on a subset, the incompleteness of property-based testing, and dependence on specification quality. Appendices F and G report the controlled comparison and repeated-run results. Guidelines: • The answer [N/A] means that the paper has no limitation while the answer [No] means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate “Limitations” section in their paper. • The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach. For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren’t acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 37

3. Theory assumptions and proofs Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: [N/A] Justification: The paper presents no theoretical results. Guidelines: • The answer [N/A] means that the paper does not include theoretical results. • All the theorems, formulas, and proofs in the paper should be numbered and crossreferenced. • All assumptions should be clearly stated or referenced in the statement of any theorems. • The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition. • Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material. • Theorems and Lemmas that the proof relies upon should be properly referenced. 4. Experimental result reproducibility Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)? Answer: [Yes] Justification: Section 4 describes both testbeds, the agents’ inputs, the model, harness, tools, and review procedure. Appendices A and B provide the full agent prompts; Appendix D reports per-application ViBench results. Appendices F and G describe the additional comparisons. Guidelines: • The answer [N/A] means that the paper does not include experiments. • If the paper includes experiments, a [No] answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not. • If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable. • Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed. • While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example (a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm. (b) If the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully. (c) If the contribution is a new model (e.g., a large language model), then there should either be a way to access this model for reproducing the results or a way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset). 38

(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results. 5. Open access to data and code Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material? Answer: [Yes] Justification: Code and data are provided as supplementary material. Independently of that, Appendix A reproduces the full prompt verbatim, which is the whole of our method, and both testbeds are publicly available. Guidelines: • The answer [N/A] means that paper does not include experiments requiring code. • Please see the NeurIPS code and data submission guidelines (https://neurips.cc/ public/guides/CodeSubmissionPolicy) for more details. • While we encourage the release of code and data, we understand that this might not be possible, so [No] is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for a new open-source benchmark). • The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https: //neurips.cc/public/guides/CodeSubmissionPolicy) for more details. • The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc. • The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only a subset of experiments are reproducible, they should state which ones are omitted from the script and why. • At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable). • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 6. Experimental setting/details Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer) necessary to understand the results? Answer: [Yes] Justification: Section 4 specifies the agents, reviewer, and taxonomy classifier. Appendices A and B give the agent prompts, Appendix D the per-application breakdown and execution environment, and Appendices F and G the additional experimental designs. Guidelines: • The answer [N/A] means that the paper does not include experiments. • The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them. • The full details can be provided either with the code, in appendix, or as supplemental material. 7. Experiment statistical significance Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments? Answer: [Yes] 39

Justification: Appendix D.3 reports a paired two-sided sign test over the 25 ViBench applications, treating each application as one paired observation: Spec-Driven PBT writes fewer tests on all 25 and reaches a higher bugs-per-test ratio on all 25, p ≈ 6 × 10−8 in both cases. Appendix G reports results from three runs per method. Guidelines: • The answer [N/A] means that the paper does not include experiments. • The authors should answer [Yes] if the results are accompanied by error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper. • The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions). • The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. • It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors is not verified. • For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g., negative error rates). • If error bars are reported in tables or plots, the authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text. 8. Experiments compute resources Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed to reproduce the experiments? Answer: [Yes] Justification: Appendix D.4 gives the executor configuration — one Modal sandbox per generation cell, a Linux/amd64 Docker container with 2 cores and 4 GiB of memory running Ubuntu 24.04, no accelerators — together with agent wall-clock time, token counts and API cost, reported per cell and in total for each method. Guidelines: • The answer [N/A] means that the paper does not include experiments. • The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage. • The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute. • The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn’t make it into the paper). 9. Code of ethics Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? Answer: [Yes] Justification: The research conforms with the NeurIPS Code of Ethics in every respect. Guidelines: • The answer [N/A] means that the authors have not reviewed the NeurIPS Code of Ethics. • If the authors answer [No], they should explain the special circumstances that require a deviation from the Code of Ethics. 40

• The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 10. Broader impacts Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed? Answer: [Yes] Justification: The Conclusion states the positive impact: the method contributes to the verifiability of agentic coding by surfacing, in the specification’s own vocabulary, the requirements an implementation breaks. Section 7 names the corresponding risk: propertybased testing is not exhaustive, so a suite that passes is not evidence of correctness, and nothing in this work argues that human review can be dispensed with. We are aware of no other negative societal impact specific to the method; it produces failing tests and bug reports for code the user already controls, and the defects discussed here are in benchmark applications rather than deployed systems. Guidelines: • The answer [N/A] means that there is no societal impact of the work performed. • If the authors answer [N/A] or [No], they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate Deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 11. Safeguards Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pre-trained language models, image generators, or scraped datasets)? Answer: [N/A] Justification: The paper releases no pretrained model, scraped dataset or generative artefact carrying a risk of misuse. The bugs discussed are in benchmark applications, not in deployed software, so no disclosure process applies. Guidelines: • The answer [N/A] means that the paper poses no such risks. • Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. 41

• We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort. 12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected? Answer: [Yes] Justification: ViBench [Zhong et al., 2026], PBTBench [Jing et al., 2026], Hypothesis [MacIver et al., 2019] and the Agentic PBT baseline [Maaz et al., 2025] are each cited where used, and are used within their terms. Guidelines: • The answer [N/A] means that the paper does not use existing assets. • The authors should cite the original paper that produced the code package or dataset. • The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset. • For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. • If this information is not available online, the authors are encouraged to reach out to the asset’s creators. 13. New assets Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets? Answer: [Yes] Justification: The prompt that constitutes our method is documented in full in Appendix A. The code, the generated test suites and the run artifacts accompany the submission as supplementary material. Guidelines: • The answer [N/A] means that the paper does not release new assets. • Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file. 14. Crowdsourcing and research with human subjects Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)? Answer: [N/A] Justification: The paper involves no crowdsourcing and no research with human subjects. Guidelines: • The answer [N/A] means that the paper does not involve crowdsourcing nor research with human subjects. 42

• Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included in the main paper. • According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector. 15. Institutional review board (IRB) approvals or equivalent for research with human subjects Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained? Answer: [N/A] Justification: The paper involves no research with human subjects, so no review was required. Guidelines: • The answer [N/A] means that the paper does not involve crowdsourcing nor research with human subjects. • Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 16. Declaration of LLM usage Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigor, or originality of the research, declaration is not required. Answer: [Yes] Justification: LLMs are the object of study and the core of the method, not an incidental tool. Sections 3 and 4 describe the agents, the LLM reviewer, and the taxonomy classifier, which use Claude Opus 5 through the Claude Code harness. Appendices A and B provide the agents’ full prompts. Guidelines: • The answer [N/A] means that the core method development in this research does not involve LLMs as any important, original, or non-standard components. • Please refer to our LLM policy in the NeurIPS handbook for what should or should not be described.

43

Related documents

• Spec-Driven PBT: Deriving Semantic Invariants from Code Specifications for Agentic Property-based Testing#1659501
• PBT-Bench: Benchmarking AI Agents on Property-Based Testing#1217464
• Practical Implementation Report on Introducing Spec-Driven Development Using AI Agents in Software Development PBL#622599
• AI-Driven Test Automation Frameworks for the Modern Software Quality Engineering#408663
• Beyond Component Testing: Validating Agentic AI Systems#422295