SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "SPINACH: Inferring Properties ..."
SPINACH: Inferring Properties of Web Applications for Property-Based Testing
Savitha Ravi and Michael Coblenz
(University of California at San Diego, USA)
Turning AI-generated web application prototypes into reliable, deployable software requires testing, yet writing property-based tests (PBTs) is difficult: developers struggle to identify meaningful properties, and LLMs asked to generate tests from natural language documentation often miss relevant ones. We present Spinach, a VSCode extension that addresses this gap via a specification inference pipeline. An LLM agent first explores a web application and represents its functionality as software concepts, a user-facing behavioral specification. A second agent derives natural language properties from these concepts for developer review; a final phase translates approved specifications into LTL and executable PBTs using the Bombadil framework. We ask whether high-level conceptual specifications improve LLM-generated PBT quality (RQ1) and whether they help developers extend and maintain AI-generated systems (RQ2). We report preliminary results applying Spinach to two open-source applications, RealWorld and 4ga Boards, and outline planned evaluations using mutation testing and a user study of human-AI collaborative development.
Article Search
Article: splashws26specopsmain-p9-p (type: Short Paper (4 pages + 1 page for references)) doi:10.1145/3842652.3843198
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "RuSMT: An Executable Semantics ..."
RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer
Mehrad Haghshenas and Meng Xu
(University of Waterloo, Canada)
Conformance testing asks whether an implementation agrees with its specification. When the specification is expressed in prose, one established approach is to mechanize it as an executable specification. This executable then serves as the oracle, and an input on which an implementation disagrees with it is a potential bug, either in the implementation or in the mechanized specification itself. How those inputs are obtained matters, because an oracle can only adjudicate the inputs it receives. Inputs can be derived from the specification itself, and coverage-guided generators can drive aggregate coverage high. But aggregate coverage does not provide a way to target a specific condition in the specification and generate an input that reaches it. This matters particularly for error conditions, where implementations are known to diverge and where the code is empirically under-tested.
This paper presents RuSMT, a framework for encoding prose specifications as executable oracles using a domain-specific language embedded in Rust. Its DSL provides types denoting Z3 sorts and primitives corresponding to Z3's operations. Concretely, the author writes the specification and marks a branch with a named marker, which identifies a path condition for the backend test synthesizer. In this paper, markers always identify error conditions. The same program is therefore used in two ways: compiled by rustc, it executes as the conformance oracle; lowered to SMT-LIB it yields one reachability query per marker. Z3 then solves each query: a sat model is rendered by a printer into a test program in the specified language, while unsat indicates that the marker is unreachable. If Z3 returns unknown or times out, RuSMT invokes a language model to propose a concrete candidate based on the emitted SMT-LIB and Z3's previous verdicts. The candidate is added to the original query as a single equality, thus constraining the search. If the candidate is rejected, its result is fed back to the language model to propose a new candidate. The process repeats until the fixed budget is exhausted.
We write two executable specifications in the DSL: IMP, Winskel's canonical small imperative language as a small end-to-end demonstration, and a TOML 1.1.0 parser, implemented from the published specification. We mark 2 branches in the IMP program and 183 in the TOML parser. Z3 alone solves both IMP queries. It solves none of the 183 TOML queries within our available computational budget: lowering the recursive parser as a whole effectively turns the problem into bounded model checking, whose formula-size blowup is well known. With the language model in the loop, RuSMT reaches 146 of the 183.
We ran the TOML-generated test suite against four independent TOML parsers and found divergences on 12 inputs. Of these, 9 test behaviour the specification leaves open, such as integer width and float exponent range, so they are not conformance obligations. The remaining three are implementation defects, 1 of which was previously unreported. The unreported defect was found in smol-toml, which accepts an array-of-tables header closed by a single bracket; we have reported this issue upstream.
Article Search
Artifacts Available
Article: splashws26specopsmain-p5-p (type: Full Paper) doi:10.1145/3842652.3843196
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Specifications for Humans, ..."
Specifications for Humans, Agents, and Tooling
Mark Marron
(University of Kentucky, USA)
Specifications are the central mechanism for communicating intents, requirements, and constraints in software development. When they are explicit, clear, and reliable, they are an effective means for collaboration and cooperation. They allow for stakeholders to specify what they want, developers (or AI agents) to understand and implement the needed functionality, for clients to effectively use the system, and for automated tooling to validate the correctness for each of these steps.
This tool paper outlines the Bosque API (BAPI) ecosystem, a software ecosystem designed to support modern spec-centered development. The BAPI specification language works in a fully polyglot ecosystem and provides a suite of features, including unparalleled expressivity, test generation, validation, and sand-boxing to support the complete application development lifecycle. These are critical to supporting emerging security and coding (both API implementation & usage) challenges presented by agentic AI systems.
Article Search
Article: splashws26specopsmain-p3-p (type: Full Paper) doi:10.1145/3842652.3843194
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "SPINACH: Inferring Properties ..."
SPINACH: Inferring Properties of Web Applications for Property-Based Testing
Savitha Ravi and Michael Coblenz
(University of California at San Diego, USA)
Turning AI-generated web application prototypes into reliable, deployable software requires testing, yet writing property-based tests (PBTs) is difficult: developers struggle to identify meaningful properties, and LLMs asked to generate tests from natural language documentation often miss relevant ones. We present Spinach, a VSCode extension that addresses this gap via a specification inference pipeline. An LLM agent first explores a web application and represents its functionality as software concepts, a user-facing behavioral specification. A second agent derives natural language properties from these concepts for developer review; a final phase translates approved specifications into LTL and executable PBTs using the Bombadil framework. We ask whether high-level conceptual specifications improve LLM-generated PBT quality (RQ1) and whether they help developers extend and maintain AI-generated systems (RQ2). We report preliminary results applying Spinach to two open-source applications, RealWorld and 4ga Boards, and outline planned evaluations using mutation testing and a user study of human-AI collaborative development.
Article Search
Article: splashws26specopsmain-p9-p (type: Short Paper (4 pages + 1 page for references)) doi:10.1145/3842652.3843198
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "Grounding AI Agents in Contracts: ..."
Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation
Michele Tufano, James McClure, José Cambronero, Runxiang Cheng, Sherry Shi, Renyao Wei, Dorothy Chen, Franjo Ivancic, Livio Dalloro, and Pat Rondon
(Google, USA)
LLM-based agents are increasingly used for coding tasks, where they have outperformed many classical approaches and scaled to repository-level tasks, such as test generation. However, when directly prompted to generate tests, these agents can fail to reason about the code and its underlying contracts, thereby missing edge cases and behavioral boundaries that affect test quality. To address this limitation, we propose Spec-Driven Test Generation, where we instruct an agent to first reason about – and explicitly document – code pre-conditions, post-conditions, and undefined behaviors. This intermediate semi-formal specification acts as a cognitive scaffold to guide subsequent test generation. Our evaluation on production bugs from Google shows that the spec-driven agent can deliver a 9.8 percentage points (p = 0.0352) improvement in bug detection rate and a 2.5 percentage point (p = 0.0034) improvement in branch coverage, compared to a traditional test generation agent baseline. Using LLM-as-a-Judge, we further show that test suites generated by the spec-driven agent are superior to the baseline and human-authored tests in 77.8% and 56.7% of the cases, respectively, and demonstrated improvements on following best practices, readability, and edge-case coverage.
Article Search
Article: splashws26specopsmain-p4-p (type: Full Paper) doi:10.1145/3842652.3843195
SpecOps '26: "RuSMT: An Executable Semantics ..."
RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer
Mehrad Haghshenas and Meng Xu
(University of Waterloo, Canada)
Conformance testing asks whether an implementation agrees with its specification. When the specification is expressed in prose, one established approach is to mechanize it as an executable specification. This executable then serves as the oracle, and an input on which an implementation disagrees with it is a potential bug, either in the implementation or in the mechanized specification itself. How those inputs are obtained matters, because an oracle can only adjudicate the inputs it receives. Inputs can be derived from the specification itself, and coverage-guided generators can drive aggregate coverage high. But aggregate coverage does not provide a way to target a specific condition in the specification and generate an input that reaches it. This matters particularly for error conditions, where implementations are known to diverge and where the code is empirically under-tested.
This paper presents RuSMT, a framework for encoding prose specifications as executable oracles using a domain-specific language embedded in Rust. Its DSL provides types denoting Z3 sorts and primitives corresponding to Z3's operations. Concretely, the author writes the specification and marks a branch with a named marker, which identifies a path condition for the backend test synthesizer. In this paper, markers always identify error conditions. The same program is therefore used in two ways: compiled by rustc, it executes as the conformance oracle; lowered to SMT-LIB it yields one reachability query per marker. Z3 then solves each query: a sat model is rendered by a printer into a test program in the specified language, while unsat indicates that the marker is unreachable. If Z3 returns unknown or times out, RuSMT invokes a language model to propose a concrete candidate based on the emitted SMT-LIB and Z3's previous verdicts. The candidate is added to the original query as a single equality, thus constraining the search. If the candidate is rejected, its result is fed back to the language model to propose a new candidate. The process repeats until the fixed budget is exhausted.
We write two executable specifications in the DSL: IMP, Winskel's canonical small imperative language as a small end-to-end demonstration, and a TOML 1.1.0 parser, implemented from the published specification. We mark 2 branches in the IMP program and 183 in the TOML parser. Z3 alone solves both IMP queries. It solves none of the 183 TOML queries within our available computational budget: lowering the recursive parser as a whole effectively turns the problem into bounded model checking, whose formula-size blowup is well known. With the language model in the loop, RuSMT reaches 146 of the 183.
We ran the TOML-generated test suite against four independent TOML parsers and found divergences on 12 inputs. Of these, 9 test behaviour the specification leaves open, such as integer width and float exponent range, so they are not conformance obligations. The remaining three are implementation defects, 1 of which was previously unreported. The unreported defect was found in smol-toml, which accepts an array-of-tables header closed by a single bracket; we have reported this issue upstream.
Article Search
Artifacts Available
Article: splashws26specopsmain-p5-p (type: Full Paper) doi:10.1145/3842652.3843196