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

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 writes 2.4$\times$ fewer property tests than Code-driven PBT while surfacing more candidate bugs, with 2.7$\times$ as many bugs found per test. The two approaches also find largely different bugs: nearly 60\% of the 169 distinct 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.