Bug Finding With Agentic Symbolic Execution

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

Bug Finding with Agentic Symbolic Execution George Granberry, Wolfgang Ahrendt, Moa Johansson

Andrew D. Gordon

Chalmers University of Technology Gothenburg, Sweden {georgegr, ahrendt, moa.johansson}@chalmers.se

University of Edinburgh Edinburgh, United Kingdom andy.gordon@ed.ac.uk

the symbolic environment. Candidates judged to be application bugs are turned into test cases, validated as witnesses by concrete execution, and reported to the user. We target database-backed web applications written in Python, a popular class of software whose behavior depends on external calls and which symbolic analysis has therefore rarely reached. We evaluate on 1,156,044 lines of Python in 11 popular open-source applications (Zulip, NetBox, Apache Superset, and others), against a purely LLM-based baseline, and ask: 1) RQ1 (Reach): What fraction of the contracted functions can symbolic execution execute with agentic environment synthesis, compared to without it? 2) RQ2 (Exploration depth): How deeply does symbolic execution explore the functions it executes, and what does it report? 3) RQ3 (Bugs): What bugs does symbolic execution find in this code, and which of them does direct LLM inspection miss? a) The need for hand-written models: Symbolic-execution research has long had answers to the problems that stop an engine on real code: environment models and mocks for calls the engine cannot follow [2], [3], symbolic treatment of database state [4]–[6], and lazy initialization for inputs that I. I NTRODUCTION are complex objects [7]–[9]. Each must be instantiated for Contracts (pre- and postconditions) let a symbolic execution every project: someone has to write the stubs, the invariants engine check code automatically: the engine propagates con- that bound a lazily built object, and the model of the external straints along each path and asks an SMT solver for an input system. This per-project manual work is a large part of why that violates a contract, which it returns as a counterexample. these techniques have rarely reached large database-backed Two things stand in the way on real applications. Their code applications. b) Our idea: We use an agent as the missing instantiation ships without contracts, and code that calls into an external system such as a database cannot run symbolically without layer. Rather than taking an environment model as input, our a model of that system. CrossHair [1], a symbolic execution pipeline produces it, through knowledge-seeded environment engine for Python, needs both. Our work makes symbolic synthesis: the model is seeded by framework knowledge execution available, with full automation, to code that has packaged in the agent’s skills and by the agent’s own inspection of the repository, and checked by loading it into CrossHair. neither contracts nor models of its external calls. Our neuro-symbolic agent crosshair-bugs combines LLM- The same agent writes the contracts that serve as the oracle, based specification generation with symbolic execution. The and executable witnesses against the real application discharge agent writes a contract for each function and a symbolic whatever the over-approximate model admits. c) Findings: RQ1 (Section V-A and Fig. 4): bare model of the database the function touches, and CrossHair then searches for inputs that violate the contracts. Every resulting CrossHair executes 4.5% of the 5,406 contracted functions, and bug candidate is judged by a separate audit agent, which the framework initialization a test suite performs 29.5%. With attributes it to the application, to the generated contract, or to the synthesized environment it executes 81%. RQ2 (Section V-B and Fig. 5): 28.6% of the functions are explored to at least Preprint under review. 25 paths without a violation, and 3.6% exhaustively. 39.1%

Abstract—Symbolic execution, in tools such as CrossHair for Python, is a powerful technique for finding bugs, but two barriers hinder its adoption: the human effort of annotating code with assertions, and the need to model the execution environment outside Python, such as an external database. To overcome both, we design an agentic harness that orchestrates the symbolic execution tool CrossHair together with an AI coding agent. Without human intervention, it instruments a repository with assertions, synthesizes a constraint-aware symbolic environment for the database, runs symbolic execution, and constructs a concrete test as evidence for each bug it reports. We evaluate our harness on 1,156,044 lines of Python code over 11 popular opensource Python web applications (Zulip, NetBox, Apache Superset, and others). With the synthesized environment, CrossHair executes 81% of the 5,406 contracted functions, against 4.5% without it. Our pipeline finds 1,050 bugs, each reproduced by a test against the unmodified application, 221 of them by CrossHair, and 312 of them are missed by a baseline in which the same LLM inspects the code. The two find different kinds of bugs: CrossHair’s are mostly crashes on input-domain corner cases that validation admits, such as empty strings, missing fields and unusual characters, while inspection’s are mostly bugs that produce wrong output. Our framework thus lets symbolic execution supplement inspection-based bug finding. Index Terms—symbolic execution, LLM agents, databasebacked web applications, formal methods, environment synthesis

agentic harness + skill library generate 1

Environment Synthesis (stubs + lazy init)

# models.py class Currency(Model): rate = DecimalField() def save(self, *a): super().save(*a)

# schema IR Currency.rate: max_digits=10 null=False

# stubs.py Currency.save = mock_save add(rate >= 0)

run

3

4

Symbolic Execution

schema

judge

Audit

validate

5 accepted

Witness Validation

Report

contracted function

2

Contract Generation

# models.py def save(self): """post: rate >= 0""" flagged defects

Fig. 1. System overview.

are refuted, but most refutations are false positives of the over-approximate environment, which the audit removes. RQ3 (Section V-C and Figs. 7 and 8): the pipeline finds 1,050 bugs, each reproduced against the unmodified application and 920 of them end-to-end: 221 found by CrossHair and 829 flagged while writing contracts. A baseline that asks the same model to inspect the code reproduces more bugs (1,824) but misses 312 of ours, including a third of CrossHair’s. The two effects meet in 110 of CrossHair’s bugs, which lie in functions that execute only under the synthesized environment. The baseline misses 40 of these, so neither tool alone would have found them. Our contributions are: • Knowledge-seeded environment synthesis for ORM call sites: an agent builds a symbolic model of the database from framework knowledge and repository inspection, and repairs it until CrossHair can load it (Section III-B). • Agent-instantiated symbolic-execution techniques: schemaconstrained ORM stubs, and bounded lazy initialization whose bounds the agent infers from the code, installed through CrossHair’s plugin interface without modifying the engine (Section III-B). • A design principle, the LLM proposes, the solver checks, concrete execution confirms, realized as a reproducible agent harness (Sections III-A and III-F). • An evaluation on 1,156,044 lines of Python in 11 web applications, reporting reach, exploration depth, and the 221 witness-reproduced bugs symbolic execution finds, compared against a same-model, witness-validated LLM baseline. d) Scope of the claim: We do not argue that symbolic execution finds more or more important bugs than an LLM reading the code: on our corpus it does not. We show that, once an agent supplies the environment, symbolic execution runs on large, complex database-backed applications at scale and finds the bugs it is known for: input-domain corner cases that validation admits and that LLM inspection with the same model often misses.

II. BACKGROUND A. CrossHair CrossHair is a concolic [10], [11] analysis tool for Python that searches for inputs that violate a function’s specification [1]. Specifications are supplied as contracts seen in Fig. 3 and CrossHair attempts to find a concrete input, admitted by the pre-conditions, for which an exception is raised or a postcondition evaluates to false. Such an input is reported as a counterexample. CrossHair calls the function under test, substituting symbolic proxy objects for its arguments. A parameter annotated int, for instance, is supplied as a SymbolicInt that carries, instead of a concrete value, an SMT-LIB [12] term of sort Int over symbolic variables, which CrossHair builds through the API of the SMT solver Z3 [13]. As the function executes, operations on these symbolic types build up Z3 constraints, and the branch conditions encountered along a path are accumulated into a path condition. CrossHair then uses Z3 to identify feasible paths, and records its decisions so that subsequent executions explore alternative branches. When a target condition is reached, it queries the solver for a variable assignment satisfying the precondition and path conditions, but violating the target condition, and surfaces it to the user. CrossHair is consequently effective at discovering counterexamples and bringing higher assurance than the typical test. It does not, however, offer a guarantee of the absence of a counterexample. A contract constrains a single function, but CrossHair’s behavior at function boundaries follows directly from this execution model and governs how a misstated contract behaves. A callee’s precondition is enforced at the call site: invoking a contracted function with arguments its precondition forbids raises a precondition failure, reported against the caller (Fig. 2). A postcondition thus binds only the function it annotates, whereas a precondition additionally imposes an obligation on every caller, an asymmetry we rely on in Section III-C. Because CrossHair’s symbolic types mirror the semantics of Python’s built-ins, any code whose behavior reduces to those

def callee(x: int) -> int: ’’’pre: x >= 0’’’ return x def caller(z: int) -> int: ’’’post: True’’’ return callee(z - 10) # PreconditionFailed: "x >= 0" not satisfied

commands and observe the results, so that it can carry out multistep software engineering tasks through an agent–computer interface [14]. Agent Skills package the procedural knowledge for a specialized task into a loadable unit [15]: a directory with a SKILL.md of natural-language instructions that the agent loads on demand, together with optional scripts and references. III. M ETHODOLOGY

Fig. 2. How CrossHair handles a callee’s contract during a caller’s analysis. A callee’s precondition is checked at the call site: reaching callee with a negative argument makes caller fail, so an over-strong precondition shows up when a caller is analyzed.

A. System Overview

Figure 1 and Algorithm 1 show our pipeline in five stages, which the rest of this section follows in order. (1) Environment synthesis models the database and the framework so that CrossHair can execute the code that uses them (Section III-B). def order_balance(order_id: int) -> int: ’’’ (2) Contract generation writes a contract into each function pre: order_id > 0 under test, guided by the schema from stage 1, and records post: _ >= 0 functions the agent already judges defective (Section III-C). ’’’ (3) Symbolic execution runs CrossHair on every contracted order = Order.objects.get(pk=order_id) function, without model calls (Section III-D). (4) An audit return order.subtotal - order.discount agent judges each CrossHair finding and each flagged defect, Fig. 3. Contract-annotated function from a hypothetical store application. and (5) a witness test confirms each real bug against the order_balance is coupled to the ORM and cannot be executed without a unmodified application (Section III-E). Each subsection names model of the database environment. the steps of its stage in Algorithm 1, agent steps in SMALL CAPS and script steps in sans-serif. Section III-F describes the harness that runs them. built-ins can be executed symbolically, including pure-Python The stages follow one design principle: the LLM proposes, implementations drawn from the standard library and thirdthe solver checks, concrete execution confirms. Stages 1 and party packages [1]. Conversely, code that reduces to Python 2 propose an environment model and a specification, either outside of the types modeled by CrossHair cannot be analyzed. of which may be wrong. Stage 3 searches for an input that The framework introduced in the remainder of this paper is violates the specification, and its verdict is only as good as aimed squarely at recovering analyzability across this boundary. both. Stages 4 and 5 remove counterexamples caused by a miscalibrated contract or by the over-approximate environment, B. Target codebases the last by running each bug against the real application. This work targets open-source Python web applications that interact with databases. Such codebases are ill-suited B. Stage 1: Environment Synthesis (Alg. 1, lines 1–4) to off-the-shelf symbolic analysis: although they are widely CrossHair can analyze only a function it can execute, and a used and actively maintained, their tight coupling to stateful function embedded in a web framework cannot run until the frameworks and database backends places much of their framework is started and its database modeled, work that has logic beyond the reach of an engine that can only reason so far been written by hand. Our agent seeds this model with about self-contained code. Most of this coupling runs through prior knowledge: the skill packages what we know about each an object-relational mapper (ORM): a library that maps supported framework (stub templates for ORM calls, start-up database rows to ordinary Python objects. To make this patterns, constructors for framework objects). A script identifies concrete, consider the function in Fig. 3, annotated with a the ORM and its model files (DetectOrm), and an agent brings CrossHair contract. CrossHair cannot execute this function sym- up the framework’s runtime from the repository’s settings bolically. The call Order.objects.get(pk=order_id) (P REFLIGHT). Agents then read the model definitions and dispatches into ORM machinery, which expects a configured migrations for the database’s constraints (S CHEMA) and encode database connection and issues SQL against a populated table. them in a constrained stub module (S TUBS, C ONSTRAIN) CrossHair has no built-in functionality to model the surrounding and a lazy-initialization plugin (LazyInit). Every artifact an environment or database, so this will fail to execute. Notably, agent writes passes a script check (compilation, contract lint, the post-condition is exactly the kind of property we would a CrossHair parse), and the agent repairs reported failures. like to check (a discount exceeding the subtotal would make The central obstacle is the database. A call into the the balance negative), but it is unreachable without a model of persistence layer leaves Python entirely, issuing SQL against a the ORM function. database that has no concept of symbolic values. The same is C. Coding agents and skills A coding agent is an LLM embedded in a control loop, or harness, that gives it tools to read and write files, run shell

true of any boundary the language cannot follow (an HTTP request, a C extension, a read from the filesystem), and the technique we describe could apply to all of them, but we model the database.

Algorithm 1: The crosshair-bugs pipeline, in the five stages of Fig. 1. S MALL CAPS are agent steps (a fixed prompt whose result must validate against a JSON Schema), sans-serif are script steps, and ∥ marks one agent per item. Gatek (x) checks an agentwritten artifact x with a script (compilation, contract lint, CrossHair parse) and on failure hands the report to a repair agent, at most k times. δ is the detected ORM, F its model files, e the runtime configuration, Σ the schema constraints, S the stub module, L the lazy-initialization plugin, β the budget of functions to contract, I the defects the planner flags, and Ω and B CrossHair’s outcomes and findings. Input: codebase C Output: report R, contracted source // Stage 1: environment synthesis (δ, F)S← DetectOrm(C); e ← P REFLIGHT(C, δ); 2 Σ← {S CHEMA(m, δ) | m ∈ F} ; //
∥ 3 S ← Gatek C ONSTRAIN (Gatek (S TUBS (F, δ)), Σ) ;
4 L ← LazyInit Σ, I NVARIANTS (F , Σ) ; 1

// Stage 2: contract generation T ← Rank(TARGETS(C), β); I ← ∅; 6 repeat 7 foreach a ∈ Chunk(Pending(T )) do // ∥ 8 (pa , Ia ) ← P LAN(a, δ, Σ); I ← I ∪ Ia ; 5

foreach g ∈ ByFile({pa }) do Gatek (A PPLY(g)) ∥; Gatek (Lint(C)); 11 until Pending(T ) = ∅; 9

10

12

// Stage 3: symbolic execution O ← CrossHair(C, S, L, e); (Ω, B) ← Classify(O);

13

// Stage 4: audit
J ← R ECONCILE {AUDIT(b) | b ∈ B ∪ I} ;

// Stage 5: witness validation foreach b ∈ J judged a real bug do 15 wb ← W ITNESS U NIT(b); 16 if wb reproduces then wb ← wb ∪ W ITNESS E2E(b);

14

17 18

// ∥ // ∥

R ← Report(Ω, J , w); return R, contracted source;

Our approach, sketched in Fig. 1, is to have the agent interpose import-time stubs, a form of mock installed by monkey-patching, on the ORM calls that the symbolic engine cannot execute. A stub intercepts the call that would have reached the database and supplies a value in its place, so that execution continues through the logic that consumes it. The decisive question is what that value should be. A stub could return a concrete value. This lets the function run, but it collapses the symbolic state onto a single path. At the opposite extreme, a stub could return an unconstrained symbolic value, which the engine is free to explore in full. We take the

middle path: the stub returns a constrained symbolic value. The agent searches the repository for evidence of constraints the database itself would enforce on any persisted row and imposes them on the symbolic value the stub returns. a) Lazy initialization of ORM and framework objects: Stubs supply values for calls into the database, but many functions also receive database-backed objects as arguments: a model instance as self, a related object, a request or a form. CrossHair synthesizes arguments from type annotations by running the class constructor on symbolic inputs, which for ORM models and framework classes usually fails, so the function is never analyzed. We therefore generate a plugin that applies lazy initialization [7], [16] through CrossHair’s register_type hook, without modifying the engine. A model instance is created without running its constructor. Each field is materialized as a symbolic value on first read, and each related object is built on first traversal, up to three levels deep. Values are bounded by the harvested schema constraints and by per-field invariants that an agent extracts from validators, choices and forms (I NVARIANTS), a form of bounded lazy initialization [8], [17], [18]. In classic bounded lazy initialization these bounds, like the class invariants of generalized symbolic execution, are written by hand, whereas here the agent infers them from the code. Classes whose constructor cannot run receive an under-constrained instance whose attributes are synthesized on first access [9], and framework objects (requests, sessions, forms, administrative contexts) receive symbolic stand-ins. Stubbed query results are drawn from the same lazy instances, so a lookup returns rows that satisfy it. The plugin is a fixed part of the harness, the same for every project. Only the list of model classes and the agent-extracted invariants it is filled with are project-specific. This model is deliberately an over-approximation—meaning we constrain each stubbed call on its own, to the invariants the schema guarantees, and beyond keeping repeated queries on one execution path consistent, we do not model the database as a stateful store. We accept instead that the over-approximation admits some infeasible executions and discharge the resulting false positives downstream, through triage and concrete witness validation, rather than through heavier stub machinery. C. Stage 2: Contract Generation (Alg. 1, lines 5–11) CrossHair reports a violation only relative to a specification supplied from outside [19], and real-world code ships without one. This stage removes that barrier by having the agent synthesize the specifications. Given an existing function, the agent reads its body along with the surrounding context and emits a contract, annotating the source code without changing the code itself. Concretely the agent enumerates the functions worth contracting (TARGETS), and a script ranks them, keeps at most β (Rank) and divides them into batches (Chunk). Within a batch, a planning subagent drafts a contract for each function, using the schema constraints from stage 1 (P LAN), and the resulting plans are grouped by source file (ByFile) so a single applier writes all of a file’s contracts in one pass (A PPLY). While planning, the agent also records functions it

judges defective (I), which are audited alongside CrossHair’s medium: observable wrong behavior; low: real but covered findings. by upstream validation), predicts whether the bug is reachable A contract is valuable only insofar as it captures what from a public entry point or latent, and records whether its a function is meant to do, not what its code literally does. discovery depended on the ORM model. Both labels are the Recovering that intent is the part of the task we ask the agent LLM’s judgment, and no human reviews them during the run. to perform: it reads past the implementation, grounding the A consistency pass then reviews the verdicts of each package inference in type annotations, docstrings, parameter and return together and corrects contradictions (R ECONCILE). Findings names, how callers consume the result, and the validation the attributed to the environment or to the contract are not reported. code already performs, and states the abstraction behind it as b) Witness validation (lines 14–18): Each bug the audit a checkable property. This places real weight on the agent’s judges real then receives an executable test against a nonability to abstract, which varies from function to function. symbolic instance of the application. A unit witness calls the Synthesis with an LLM is heuristic. A miscalibrated contract function directly (W ITNESS U NIT). Every bug it reproduces therefore surfaces as evidence to be triaged, not a verdict to also receives an end-to-end witness that tries to trigger the be trusted. Three of the four miscalibration modes are self- failure through a public entry point of the running application revealing. An over-permissive precondition or an over-strong (W ITNESS E2E), which decides whether the bug is user-facing postcondition yields a concrete counterexample, which the or latent and checks the audit’s prediction. A bug counts as audit attributes to the contract rather than to the code, and an confirmed only if a witness reproduces it, which grounds every over-restrictive precondition is exposed when an analyzed caller reported finding in concrete program behavior rather than in passes inputs that the precondition excludes, which CrossHair an artifact of the symbolic environment. reports as a precondition failure in the caller (Section II-A). The exception, however, is a postcondition that asserts too F. Harness Implementation little: it raises no alarm and is a silent false negative. We implement Algorithm 1 as an agent harness: the program around the model that decides which model calls are made, With the instrumented repository in hand, the harness runs what each one receives, and what is done with its output [20]. CrossHair on each contracted function as a script step with Following [21], we build the pipeline as a workflow, in which no model calls (CrossHair). Every contracted file has already LLM calls are orchestrated through predefined code paths, as passed the contract lint and a CrossHair parse check (Lint). Agentless does for issue repair [22], rather than letting an For each condition, CrossHair either finds a counterexample, a agent direct its own process. This trades flexibility for the concrete input (including an initial database state) that violates predictability a measurement study requires. All state lives on it or raises an exception the contract does not allow, or keeps disk as structured JSON [23], so an interrupted run resumes exploring without a violation until the search space or the without repeating finished work. Every count we report is budget runs out. A search that exhausts its bounded state space computed by a script, not by the model, and the agent that is strong evidence, but not a proof, that the function meets its judges a result is never the agent that produced it [24]. Because contract under the harvested constraints. Section IV-C turns the control flow lives in code, two runs on the same repository these outcomes into the exploration tiers we report. walk the same graph over the same work list and differ only A counterexample need not be a bug. It may come from a in the content of individual model calls. Each run records contract that is too strong, from a stub that misses an ORM the hashes of its workflow scripts, the tool versions, and call or returns a row the real database could not produce, or per-phase token and time costs. The graphs are JavaScript from a symbolic value that leaks into code the engine does programs for Claude Code’s Workflow tool and use no thirdnot model. Separating these from application bugs is the job party orchestration framework. of the audit. D. Stage 3: Symbolic Execution (Alg. 1, line 12)

E. Stages 4–5: Audit and Witness Validation (Alg. 1, lines 13–18)

G. Baseline: the ai-bugs skill

a) Audit (line 13): A script first sorts CrossHair’s output For comparison we evaluate ai-bugs, a purely LLM into outcome classes and extracts the findings, i.e. counterexam- baseline that uses no contracts and no symbolic execution ples and application crashes (Classify). Each finding, together (Algorithm 2). It discovers the source files (D ISCOVER), fans with each defect the planning agent recorded during contract four bug-class subagents across each file (logic errors, edge generation, is then judged by its own audit agent (AUDIT). The cases, data integrity, error handling; F IND), filters their findings auditor reads the code, the contract and the trace, and decides with a skeptical verifier (S CREEN), and compiles the survivors whether the failure lies in the application, in the synthesized into a report (C OMPILE). It uses the same model and the same environment, or in the generated contract. For a real bug 1,429 files our pipeline contracted, in separate sessions with it also assigns a severity on a four-level scale given in its no access to our results. Every baseline bug in a function our prompt (critical: data loss, a security issue or a silent incorrect pipeline did not report is witnessed with the same unit and write; high: a wrong result or inconsistent state that propagates; end-to-end procedure as ours.

Algorithm 2: AI multi-agent bug finding, performed with no symbolic execution Input: codebase C Output: screened bug report R of candidate bugs 1 F ← D ISCOVER (C); S ← ∅; 2 foreach f ∈ F do S 3 Bf ← κ∈K F IND(f, κ); 4 if Bf ̸= ∅ then S ← S ∪ S CREEN(f, Bf ); 5 6

R ← C OMPILE(S); return R;

IV. E XPERIMENTAL E VALUATION We answer the three research questions of Section I. The unit of analysis throughout is a function, with each function having a single contract. A. Setup and Reproducibility All experiments use Claude Opus 5.5, run through Claude Code version 2.1.x. Symbolic execution is performed by CrossHair version v0.0.104, dispatching path constraints to Z3 version 4.16.0, with a budget of 30 seconds per condition and a per-function cap of 300 seconds, raised up to 900 seconds for functions with several postconditions. Each repository is a fresh clone at the study commit, with a virtual environment rebuilt from the original package freeze. The stubs, plugin and contracts under evaluation are those the harness produced, with no manual edits to its output. Within a run there is no open-ended triage loop: every repair loop is bounded (k = 2 attempts per gate), and contract generation is relaunched until no work is pending. The contract budget is 800 functions per repository, ranked by a static risk score. For zulip, the largest application, we ran a second batch of 800, giving 5,406 contracted functions in total. Bugs are counted per function, as the union over a repository’s runs. The pipeline’s LLM cost, counted per harness run, was at least $2,821 for all eleven repositories (a lower bound, as it excludes the orchestrating session). The baseline (Section III-G) cost about $712, plus $925 to witness its findings. These costs are estimated from the per-token API prices at the time of the runs, although all runs were made under a Claude subscription rather than paid per token. To enable independent replication, we provide a supplementary artifact1 containing the orchestration skills, compact captures of all instrumented repositories (as patches pinned to upstream commits), per-function run data, the AI-only baseline with its witnesses, and the scripts that compute every reported number. B. RQ1: Reach a) Terminology: A contracted function is executed if CrossHair completes at least one path through it on which a postcondition is checked, or refutes one of its conditions. It is 1 https://doi.org/10.6084/m9.figshare.32835236

blocked otherwise: the module fails to import or the framework fails to start, no input satisfying the precondition can be built, or every path aborts before the body returns. b) Environment ablation: We run every contracted function under three configurations, with the same contracts, budget and classifier. Bare runs plain crosshair check, with no plugins. Setup adds only framework initialization, done the way the project’s own test suite does it (settings module and django.setup(), or the application factory). Full is crosshair-bugs: the start-up plugin, the schema-constrained ORM stubs, lazy initialization and framework stand-ins. The setup arm separates the generic part of the environment, which a developer would write once per project, from what the agent synthesizes. C. RQ2: Exploration Depth and Outcomes We assign each contracted function one exploration tier, evaluated on the contract set the harness produced (Section III-F). Miscalibrated contracts are not corrected within the run but are identified by the audit (Section III-C). a) Exploration tiers: Let c be the number of distinct paths on which a postcondition was checked and held, read from CrossHair’s path-tree statistics, and taken as the minimum over the function’s postconditions. • Exhausted: every path was explored and every condition held, relative to the environment model. • Bounded: c ≥ 25 and no condition refuted. • Shallow: 1 ≤ c < 25 and no condition refuted. • Refuted: CrossHair reported a counterexample, an uncaught exception or a violated callee precondition. These are the candidate findings, which the audit splits into real bugs, false positives, tool artifacts (filtered automatically) and failures located only inside an installed library. • Blocked: c = 0 and nothing refuted (Section IV-B). The thresholds count paths, not a share of them: unless the search is exhausted, the total number of paths is unknown. A function with few paths can therefore be shallow even if the paths checked are most of them, for example 9 of 10 when the search stops before the last. A function whose search finishes is exhausted whatever its c. D. RQ3: Bug Yield A bug is confirmed when the audit judges it real (Section III-E) and a witness reproduces it against the real application code. A confirmed bug is user-facing if its end-toend witness triggers it through a public entry point, and latent otherwise. We report the confirmed bugs (RQ3.1), describe them (RQ3.2), and compare them with those of the inspectiononly baseline (Section III-G) (RQ3.3). V. R ESULTS A. RQ1: Reach The synthesized environment is what lets CrossHair run on these applications. Of the 5,406 contracted functions, bare CrossHair executes 243 (4.5%), framework initialization alone 1,595 (29.5%), and the full synthesized environment 4,394 (81%) (Fig. 4).

Fig. 4. Executed contracted functions per repository under three environments: bare CrossHair, framework initialization only, and full environment synthesis (crosshair-bugs). Pooled over 5,406 functions: 4.5%, 29.5% and 81%.

a) Bare and framework set-up: Bare CrossHair executes almost nothing: in three repositories not a single function, because the modules cannot be imported without a configured framework. What it does execute is code that never touches the framework, such as helpers that build SQL expressions without an application context. Framework initialization, the part a developer would write once per project, recovers about a third of the functions. What remains blocked under it is mostly argument construction: model instances whose constructor needs framework state, and string-typed annotations that CrossHair cannot resolve. b) Full environment synthesis: These are exactly what the agent-synthesized environment supplies: lazy initialization of model instances, ORM stubs and framework stand-ins. With them, every repository executes between 66% and 89% of its functions. The gain over framework set-up is largest where the code is most object-heavy, up to 69 percentage points (from 12% to 81%). B. RQ2: Exploration Depth and Outcomes Figure 5 gives the tier of every contracted function. Pooled, 39.1% are refuted, 28.6% bounded, 10.0% shallow and 3.6% exhausted; 18.7% remain blocked. a) Refutations are mostly not bugs: The audit splits the 2,113 refuted functions into 241 real bugs (4.5% of all functions), 1,281 false positives (23.7%), 562 tool artifacts filtered without an audit (10.4%) and 29 failures located only inside an installed library (0.5%). False positives are the price of an over-approximate environment: a lazily built instance or a stubbed query result that the real database could not produce, a symbolic value escaping into code that expects a concrete one, or an input that the application’s own validation rejects earlier. This is why every CrossHair finding is audited, and every finding the audit accepts as a bug is then witnessed.

Fig. 5. Exploration tier of each contracted function, per repository and pooled (n=5,406). Exhausted: all paths explored; bounded: at least 25 checked paths; shallow: 1–24; refuted: a condition was violated (candidate finding); blocked: no checked path.

b) Exploration is bounded, not exhaustive: Only 3.6% of functions are explored exhaustively; for most executed functions CrossHair checks many paths (the per-repository median ranges from 27 to 726) but does not finish within budget. A bounded verdict is therefore evidence, not a proof. The obstacles here are the classic ones of symbolic execution: path explosion, and operations outside the solver’s theories (string and regularexpression manipulation, date parsing, hashing, C extensions), which CrossHair concretizes. Each maps onto a mature line of symbolic-execution research [25], such as state merging [26], [27] and abstraction [28], [29], which an agent could in future instantiate in the same way as lazy initialization. c) Blocked functions: The remaining 18.7% are blocked mostly by gaps in the environment model or by contract defects, not by limits of symbolic execution. Further repair passes on the environment and contracts could recover many of them, but we chose not to spend the compute. C. RQ3: Bug Yield The pipeline found 1,050 witness-reproduced bugs across the 11 repositories: 221 found by CrossHair and 829 flagged by the agent while writing contracts. Our interest is mainly in the former, the bugs symbolic execution finds, but we report both because both pass the same audit and witnesses. a) From candidates to confirmed bugs (RQ3.1): Two sources feed the audit. Here a bug is counted at the function that contains it, which may be a callee of the function CrossHair was analyzing (RQ2 counts the analyzed function instead). After automatic filtering of tool artifacts, CrossHair’s findings point to 1,609 functions, of which the audit judged 226 to contain a real bug (14%). The planners flagged 1,013 functions while writing contracts, of which the audit accepted 991 (98%). Together, 1,064 functions were judged to contain a real bug.

b) Witness validation: For each of these the agent wrote a unit test that runs the real code, with no stubs. 1,050 were reproduced; 14 were not. We treat the 1,050 reproduced bugs as the confirmed yield. The agent then drove each confirmed bug through a public entry point of the running application with a real database: 920 (88%) reproduced end-to-end. The audit’s reachability labels largely held: of the bugs it had labeled user-facing, 889 of 912 were confirmed end-to-end, and 94 of the 137 it had labeled latent could not be reached. Of 45 high-ranked confirmed bugs that we checked against each project’s current code, maintainers had since fixed 22, with commits that describe the fix. c) Blind human review: One of the authors rated a stratified random sample of 50 of our confirmed bugs and 50 of the baseline’s, shuffled and without method labels. They judged 72% of ours and 70% of the baseline’s real, with no significant difference, but rated 31 of ours as crashes against 12 of the baseline’s, whose most common rating was minor. Rejected bugs were mostly judged intended or unreachable in practice, often because the user interface validates input the API admits. Across both methods, bugs reproduced end-to-end were judged real 82% of the time, those reproduced only in a unit test 4 of 18. d) Qualitative description (RQ3.2): Discovery is dominated by contract writing: 829 of the bugs (79%) were flagged by the agent while it wrote contracts, and 221 (21%) were found by CrossHair, 69 of them in functions the planner had not flagged (Fig. 7). By severity, as assigned by the audit, 689 are low, 321 medium, 39 high and 1 critical. The audit labels 204 bugs as coupled to the ORM, 84 of them found by CrossHair. The bugs CrossHair finds are input-domain corner cases: mostly missing or None fields, empty or whitespace-only strings, unusual characters (NUL, control or non-ASCII) and malformed formats. They share a root cause: a value is accepted with the right type but not sufficiently validated, while downstream code assumes more (Fig. 6). An SMT solver finds them because it explores values that validation admits but tests rarely probe. Of the 212 CrossHair bugs whose function we could match across the ablation arms, 110 (52%) lie in functions that are executable only with the synthesized environment: they are found only because the agent synthesized it. e) Comparison against the baseline (RQ3.3): The baseline’s verifier accepted 4,125 bug reports in 1,864 functions. Of these, 738 are functions where our pipeline also reproduced a bug. We witnessed the remaining 1,126, and 1,086 (96%) were reproduced, 925 of them end-to-end. The baseline therefore reproduces 1,824 bugs, more than our pipeline’s 1,050 (Fig. 8). Our pipeline finds 312 bugs the baseline misses, so running both finds 17% more bugs than the baseline alone; 257 of these are reproduced end-to-end. Of the 312, 239 were flagged while writing contracts and 73 by CrossHair. Relative to its size, CrossHair’s contribution is the least redundant: of the 69 bugs only CrossHair found, the baseline misses 45 (65%), against 29% of the bugs found only while writing contracts (Fig. 8).

The overlap is measured per function, and the two bug sets differ in kind: 57% of the baseline’s witnesses assert a wrong output and 29% a crash, while ours are 56% crashes and 30% wrong outputs (Section VI). With a current frontier model, direct inspection therefore finds more bugs, and more wrongoutput bugs in particular, while symbolic execution over a synthesized environment remains complementary: a third of its bugs are ones inspection misses. f) Bugs only symbolic execution finds: The strictest test of what symbolic execution adds is the set of bugs that neither the planner, while writing contracts, nor the baseline flagged. There are 45 such bugs. They are not marginal: 37 are reproduced end-to-end, and the audit rates 8 medium and 1 high severity. 26 of the 45 lie in functions that are executable only with the synthesized environment, so they depend on it as well as on the solver. Almost all are input-domain corner cases that a reader of the function overlooks because the offending input looks benign or out of scope. A specification parser crashes on an empty list such as {"max": []}, a malformed URL such as //[ makes urlparse raise, and a password longer than a library’s undocumented limit causes a server error (Fig. 6c). In each case the violating input passes every type and validation check before the failing line. VI. T HREATS TO VALIDITY a) Construct validity: Our oracle is synthesized, not given: each contract is the agent’s reconstruction of a function’s intended behavior, so a miscalibrated contract can manufacture a finding that no developer would call a bug. Witness validation (Section III-E) removes the findings that do not reproduce against the unmodified application, but a reproduced violation can still be one that no user can trigger, or behavior the developers intended: the blind review judged 82% of the sampled bugs that reproduced end-to-end to be real, but only 4 of the 18 that reproduced only in a unit test (Section V-C). The dual error is not caught: a postcondition that asserts too little yields no counterexample (Section III-C), so our counts are a precision-oriented lower bound, not a recall measure. “Executed” (RQ1) is only a proxy for analyzability, and RQ2 shows that executing a function is far from exploring it exhaustively. Finally, no maintainer has reviewed our reports. The 22 upstream fixes (Section V-C) were made independently of this work, and the blind review was done by one of the authors, who could not see which method found each bug but knows both pipelines. b) Internal validity: Our RQ1 ablation separates framework initialization from the agent-synthesized environment, but not the components of the latter (stubs, lazy initialization, stand-ins) from one another, so the 29.5% → 81% gain is attributable only to them jointly. The setup arm follows each project’s test configuration, and a developer might do better by hand. The split between bugs found by CrossHair and by the agent while contracting reflects where each bug surfaced in one pipeline, not an independent isolation of the two effects. c) Conclusion validity: LLM agents are stochastic, and we report one configuration per repository, with bugs pooled

(a) superset cast_to_num: an unintended Unicode symbol slips past the type guard if value.isdigit(): return int(value)

# True for ’2 ’ # int(’2 ’) -> ValueError

(HTTP 500 on /chart/data)

(b) django-crm Currency.save: a copy-paste typo corrupts persisted data # post: implies(__old__.self.is_state_currency, # self.rate_to_state_currency == 1.0) # -> counterexample if self.is_state_currency: self.is_state_currency = 1.0 # BUG: should be rate_to_state_currency (c) zulip check_password_strength: found only by CrossHair # new_password has no length limit in the API zxcvbn(password, max_length=settings.PASSWORD_MAX_LENGTH) # = 100 # 108 chars -> ValueError (HTTP 500 on PATCH /api/v1/settings)

Fig. 6. Three representative confirmed bugs. (a) Symbolic execution finds an input edge a type guard admits: str.isdigit() accepts the superscript digit ’²’ that int() rejects. (b) A synthesized postcondition exposes a typo that writes the rate into the boolean flag, silently corrupting persisted data. (c) CrossHair generated a password longer than zxcvbn’s length limit, and neither the planner nor the inspection baseline flagged this function.

Fig. 7. Reproduced bugs per repository by discovery mechanism: found by CrossHair (a counterexample or uncaught exception), or flagged by the agent while writing contracts.

Fig. 8. Reproduced bugs (functions) found by CrossHair, while writing contracts, and by the AI-only baseline with the same model (areas not to scale).

figures are for a single frontier model in one harness, at one over its runs (Section IV-A). We do not report variance across point in time. repeated runs because of their cost, which is the most direct threat to replication. Cross-method comparisons other than the VII. R ELATED W ORK human review are descriptive. d) Baseline asymmetry and external validity: The 738 A. Specification Synthesis functions in both bug sets were witnessed only through our pipeline, and are counted for the baseline without checking A growing body of work uses LLMs to synthesize the that it reports the same bug. Wrong-output witnesses, more specifications that serve as the oracle for a downstream common in the baseline, rest on the agent’s reading of intended verification tool [30]–[34]. LLM-written postconditions can behavior, which the human review checks only on a sample. distinguish buggy from correct code [35], and Richter and Both methods ran only on the files our pipeline contracted. Our Wehrheim check such contracts with CrossHair on small Python corpus is eleven popular open-source Python web applications benchmarks [36]. We apply the same kind of contract to on two ORMs (Django and SQLAlchemy). We make no claim large applications whose functions cannot run without an beyond ORM-backed Python, and the technique’s applicability environment model, and we synthesize that environment as to other boundaries (HTTP, C extensions, the filesystem) is well as the oracle. LLM-generated oracles tend to encode not evaluated. Popular projects may also be better typed the behavior the code has rather than the behavior it should and documented than typical code, which aids both contract have [37], one reason we audit every finding and require an synthesis and CrossHair’s type-driven proxies. Finally, our executable witness.

we use an over-approximate symbolic model. Differential testA synthesized oracle and environment could in principle ing has been applied to the ORM implementations themselves, drive any of several bug-finding engines, such as symbolic including Django’s and SQLAlchemy’s, with solver-generated or concolic execution, property-based testing, fuzzing [38]– records [47], whereas we test the applications built on them. [40], or deductive verification with a theorem prover [41]. For Python, automated unit-test generation has been evaluated The closest agentic alternative is property-based testing with at scale [48], and symbolic path constraints have been used agent-written properties: Maaz et al. [33] have an agent infer to guide LLM test generation [49], but neither addresses code properties of Python library functions and check them with that cannot run without a modeled database and framework. Hypothesis. We build on symbolic execution for its natural fit with declarative contracts and its concrete counterexamples. We E. Agentic Path Exploration do not compare it experimentally with property-based testing Other work places the LLM inside the symbolic-execution or the other engines. Each is a mature methodology with a loop to drive an already-running engine deeper. Agentic long history of comparison, and our aim is to make symbolic concolic execution [50] has agents summarize execution traces execution run on code it previously could not, not to argue and synthesize new path constraints, and Cottontail [51] uses that it finds better bugs than the alternatives. LLMs to shape highly structured inputs that get past complex parsers. LLMs remain unreliable at the precise reasoning full C. Environment Modeling for Symbolic Execution symbolic simulation needs [52], so these systems use the LLM Symbolic execution of database applications has a long as a heuristic guide. Others let the LLM take the solver’s place history. Emmi et al. [4] generate program inputs and database and reason about paths directly [53], or let it write specifications states together for programs that issue SQL, Pan et al. [5] that a classical analyzer then checks, as IRIS does with taint synthesize the database interactions that guide test generation, specifications for CodeQL [54]. We place the agent around a and Marcozzi et al. [6] execute SQL code symbolically over a sound engine and use it only to supply what the engine needs to relational model. SynthDB [42] synthesizes database contents run: where LLM-guided exploration makes the engine explore by program analysis to test web applications. Beyond databases, better, we make it applicable, and an LLM error surfaces for mocking frameworks such as Moles [2] isolate code from its us as a triageable false positive rather than an unsound analysis environment, and environment assumptions make unit proofs step. The two are complementary, and a tool such as Cottontail tractable [3]. For complex object inputs, generalized symbolic could exercise contracts whose inputs our engine cannot yet execution [7], [16], bounded lazy initialization [8], [17], [18] construct (Section IV-C). Concurrent work applies the same and under-constrained execution [9] build inputs on demand. division of labor to bounded model checking of C and Rust In all of these, the model of the environment, or the invariants code, adding a refinement loop over the specifications [55]. It that bound it, is an input written by a human, and the database does not measure how much of the code becomes analyzable techniques target SQL strings in Java or C# programs. In or compare against LLM inspection with the same model, and our setting there is no query text: the database is reached we do both. The same division underlies recent LLM-driven through ORM call sites whose framework semantics must be formal verification at scale: an LLM wrote machine-checked modeled. We make the model an output, synthesized by an Rocq proofs that 239 fuzz-test entry points across 123 openagent from framework knowledge and repository inspection, source libraries cannot crash, finding hundreds of bugs along and we instantiate the lazy-initialization techniques above with the way [41]. bounds the agent infers from the code. Recent work also uses LLMs to write the models a symbolic F. Neural Code Auditing and Agentic Vulnerability Discovery engine needs. SAILOR [43] has an LLM synthesize and refine LLM agents with code navigation and testing tools can KLEE harnesses (drivers, stubs and assertions) from engine find vulnerabilities in real codebases [56], [57], including feedback and confirms each crash by concrete replay, finding far zero-days found and patched autonomously in the AI Cyber more memory-safety vulnerabilities in C/C++ projects than an Challenge [58], [59]. A key challenge is false positives, which agentic baseline. Gordian [44] has an LLM write solver-friendly multi-agent cross-verification aims to reduce [60]. LLMs are stand-ins for code the solver handles poorly and partition also used to triage the warnings of static analyzers [61]–[63], unbounded heaps. Both target C programs and their memorythe role our audit plays for CrossHair’s findings, and to turn safety or coverage goals, whereas we target the ORM and bug reports into executable reproducing tests [64], [65], as our framework layer of Python web applications. witnesses do. D. Testing Database-Backed Applications VIII. C ONCLUSIONS Database-backed web applications frequently declare data constraints inconsistently across the database, the model and We showed that an agent can supply the environment models the user interface, and handle their violation poorly [45], and and contracts that symbolic execution needs, in place of a our bugs cluster at the same boundaries. Search-based system human, at the scale of more than five thousand functions. On testing can treat the database as part of the test input, inserting eleven web applications, symbolic execution over the syntherows that steer execution [46], but it runs a real database, where sized environment executes 81% of the contracted functions, B. Bug-Finding Engines

against 4.5% without it, and CrossHair finds 221 witnessreproduced bugs. A baseline that asks the same model to find bugs directly reproduces more bugs overall (1,824), but misses a third of CrossHair’s, mostly input-domain corner cases that inspection overlooks. Combining agent-written properties [33] with the synthesized environment, so that property-based testing can also reach database-backed code, is a natural next step. ACKNOWLEDGMENT This work was partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation. R EFERENCES [1] P. Schanely, “CrossHair - An analysis tool for Python that blurs the line between testing and type systems,” https://github.com/pschanely/ CrossHair, 2017, [Online; accessed 23-June-2026]. [2] J. de Halleux and N. Tillmann, “Moles: Tool-assisted environment isolation with closures,” in Objects, Models, Components, Patterns (TOOLS). Springer, 2010, pp. 253–270. [3] S. Priya, T. Kahsai, and A. Gurfinkel, “Unlocking the power of environment assumptions for unit proofs,” in Software Engineering and Formal Methods (SEFM), 2024. [4] M. Emmi, R. Majumdar, and K. Sen, “Dynamic test input generation for database applications,” in International Symposium on Software Testing and Analysis (ISSTA), 2007, pp. 151–162. [5] K. Pan, X. Wu, and T. Xie, “Guided test generation for database applications via synthesized database interactions,” ACM Transactions on Software Engineering and Methodology, vol. 23, no. 2, pp. 12:1–12:27, 2014. [6] M. Marcozzi, W. Vanhoof, and J.-L. Hainaut, “Relational symbolic execution of SQL code for unit testing of database programs,” Science of Computer Programming, vol. 105, pp. 44–72, 2015. [7] S. Khurshid, C. S. Păsăreanu, and W. Visser, “Generalized symbolic execution for model checking and testing,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ser. LNCS, vol. 2619. Springer, 2003, pp. 553–568. [8] N. Rosner, J. Geldenhuys, N. M. Aguirre, W. Visser, and M. F. Frias, “BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support,” IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 639–660, 2015. [9] D. A. Ramos and D. Engler, “Under-constrained symbolic execution: Correctness checking for real code,” in 24th USENIX Security Symposium, 2015, pp. 49–64. [10] K. Sen, D. Marinov, and G. Agha, “CUTE: A Concolic Unit Testing Engine for C,” in Proc. 10th European Software Engineering Conf. / 13th ACM SIGSOFT Int. Symp. Foundations of Software Engineering (ESEC/FSE), 2005, pp. 263–272. [11] P. Godefroid, N. Klarlund, and K. Sen, “DART: Directed Automated Random Testing,” in Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2005, pp. 213–223. [12] C. Barrett, P. Fontaine, and C. Tinelli, “The SMT-LIB standard: Version 2.6,” Department of Computer Science, The University of Iowa, Tech. Rep., 2017, available at www.SMT-LIB.org. [13] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ser. Lecture Notes in Computer Science, vol. 4963. Springer, 2008, pp. 337–340. [14] J. Yang, C. E. Jimenez, A. Wettig, K. Lieret, S. Yao, K. Narasimhan, and O. Press, “SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering,” Advances in Neural Information Processing Systems, vol. 37, pp. 50 528–50 652, 2024. [15] Anthropic, “Agent Skills,” https://agentskills.io, 2025, open standard; accessed 2026-06-03. [16] X. Deng, J. Lee, and Robby, “Efficient and formal generalized symbolic execution,” Automated Software Engineering, vol. 19, no. 3, pp. 233–301, 2012. [17] J. Geldenhuys, N. Aguirre, M. F. Frias, and W. Visser, “Bounded lazy initialization,” in NASA Formal Methods (NFM). Springer, 2013, pp. 229–243.

[18] P. Braione, G. Denaro, and M. Pezzè, “Enhancing Symbolic Execution with Built-in Term Rewriting and Constrained Lazy Initialization,” in Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, 2013, pp. 411–421. [19] E. T. Barr, M. Harman, P. McMinn, M. Shahbaz, and S. Yoo, “The Oracle Problem in Software Testing: A Survey,” IEEE transactions on software engineering, vol. 41, no. 5, pp. 507–525, 2015. [20] R. Lopopolo, “Harness Engineering: Leveraging Codex in an Agent-First World,” OpenAI Blog, https://openai.com/index/harness-engineering/, Feb. 2026, accessed 2026-11-02. [21] E. Schluntz and B. Zhang, “Building Effective Agents,” Anthropic Engineering Blog, https://www.anthropic.com/engineering/ building-effective-agents, Dec. 2024, accessed 2026-11-02. [22] C. S. Xia, Y. Deng, S. Dunn, and L. Zhang, “Demystifying LLM-based software engineering agents,” Proc. ACM Softw. Eng., vol. 2, no. FSE, 2025. [23] J. Young, “Effective Harnesses for Long-Running Agents,” Anthropic Engineering Blog, https://www.anthropic.com/engineering/ effective-harnesses-for-long-running-agents, Nov. 2025, accessed 202611-02. [24] P. Rajasekaran, “Harness Design for Long-Running Application Development,” Anthropic Engineering Blog, https://www.anthropic.com/ engineering/harness-design-long-running-apps, Mar. 2026, accessed 2026-11-02. [25] R. Baldoni, E. Coppa, D. C. D’Elia, C. Demetrescu, and I. Finocchi, “A Survey of Symbolic Execution Techniques,” ACM Computing Surveys, vol. 51, no. 3, pp. 1–39, 2018. [26] V. Kuznetsov, J. Kinder, S. Bucur, and G. Candea, “Efficient State Merging in Symbolic Execution,” Acm Sigplan Notices, vol. 47, no. 6, pp. 193–204, 2012. [27] D. Trabish, N. Rinetzky, S. Shoham, and V. Sharma, “State Merging with Quantifiers in Symbolic Execution,” in Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023, pp. 1140–1152. [28] S. Anand, C. S. Păsăreanu, and W. Visser, “Symbolic Execution with Abstraction,” International Journal on Software Tools for Technology Transfer, vol. 11, no. 1, pp. 53–67, 2009. [29] D. Shannon, S. Hajra, A. Lee, D. Zhan, and S. Khurshid, “Abstracting Symbolic Execution with String Analysis,” in Testing: Academic and Industrial Conference Practice and Research Techniques-MUTATION (TAICPART-MUTATION 2007). IEEE, 2007, pp. 13–22. [30] L. Ma, S. Liu, Y. Li, X. Xie, and L. Bu, “SpecGen: Automated Generation of Formal Program Specifications via Large Language Models,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 16–28. [31] S. Ugare, T. Suresh, S. Misailovic, and J. Vanegue, “Fun2spec: Code Contract Synthesis At Scale,” in Companion Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering (FSE Companion ’26), Industry Track. ACM, 2026. [32] T. Suresh, D. Korczynski, and J. Vanegue, “Agentic Separation Logic Specification Synthesis,” arXiv preprint arXiv:2605.27531, 2026. [33] M. Maaz, L. DeVoe, Z. Hatfield-Dodds, and N. Carlini, “Agentic PropertyBased Testing: Finding Bugs Across the Python Ecosystem,” arXiv preprint arXiv:2510.09907, 2025. [34] G. Granberry, W. Ahrendt, and M. Johansson, “Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis,” Formal Aspects of Computing, vol. 38, no. 2, pp. 1–36, 2026. [35] M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, “Can large language models transform natural language intent into formal method postconditions?” Proc. ACM Softw. Eng., vol. 1, no. FSE, 2024. [36] C. Richter and H. Wehrheim, “Beyond postconditions: Can large language models infer formal contracts for automatic software verification?” arXiv:2510.12702, 2025. [Online]. Available: https: //arxiv.org/abs/2510.12702 [37] M. Konstantinou, R. Degiovanni, and M. Papadakis, “Can we find bugs using LLM-generated oracles?” arXiv:2410.21136, 2024. [Online]. Available: https://arxiv.org/abs/2410.21136 [38] J. Park and I. Yun, “Agentic Fuzzing: Opportunities and Challenges,” arXiv preprint arXiv:2605.10074, 2026. [39] Y. Zhang, J. Wang, D. Berzin, M. Mirchev, D. Liu, A. Arya, O. Chang, and A. Roychoudhury, “Fixing Security Vulnerabilities with AI in OSSFuzz,” arXiv preprint arXiv:2411.03346, 2024. [40] Y. Jiang, J. Liang, F. Ma, Y. Chen, C. Zhou, Y. Shen, Z. Wu, J. Fu, M. Wang, S. Li et al., “When Fuzzing Meets LLMs: Challenges and

Opportunities,” in Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024, pp. 492– 496. [41] K. Lucas, A. Lynch, L. Tong, L. Champine, Z. Straznickas, D. Distefano, H. Agrawal, E. Ben Asher, A. Howell, S. Jawhar, C. Rohlf, N. Zeldovich, N. Carlini, R. Agrawal, and J. Gross, “LLMs are making formal software verification feasible at a much larger scale,” Anthropic Frontier Red Team, https://www.anthropic.com/research/formal-verification, Oct. 2026, accessed 2026-11-05. [42] A. Chen, J. Lee, B. Chaulagain, Y. Kwon, and K. H. Lee, “SynthDB: Synthesizing database via program analysis for security testing of web applications,” in Network and Distributed System Security Symposium (NDSS), 2023. [43] M. Shafiuzzaman, A. Desai, W. Guo, and T. Bultan, “Guiding symbolic execution with static analysis and LLMs for vulnerability discovery,” arXiv:2604.06506, 2026. [Online]. Available: https: //arxiv.org/abs/2604.06506 [44] D. S. Bouras and S. Mechtaev, “Defusing logic bombs in symbolic execution with LLM-generated ghost code,” arXiv:2603.19239, 2026. [Online]. Available: https://arxiv.org/abs/2603.19239 [45] J. Yang, U. Sethi, C. Yan, A. Cheung, and S. Lu, “Managing data constraints in database-backed web applications,” in International Conference on Software Engineering (ICSE), 2020, pp. 1098–1109. [46] A. Arcuri and J. P. Galeotti, “Handling SQL databases in automated system test generation,” ACM Trans. Softw. Eng. Methodol., vol. 29, no. 4, 2020. [47] T. Sotiropoulos, S. Chaliasos, V. Atlidakis, D. Mitropoulos, and D. Spinellis, “Data-oriented differential testing of object-relational mapping systems,” in International Conference on Software Engineering (ICSE), 2021, pp. 1535–1547. [48] S. Lukasczyk, F. Kroiß, and G. Fraser, “An empirical study of automated unit test generation for Python,” Empirical Software Engineering, vol. 28, no. 2, p. 36, 2023. [49] G. Ryan, S. Jain, M. Shang, S. Wang, X. Ma, M. K. Ramanathan, and B. Ray, “Code-aware prompting: A study of coverage-guided test generation in regression setting using LLM,” Proc. ACM Softw. Eng., vol. 1, no. FSE, 2024. [50] Z. Luo, H. Zhao, D. Wolff, C. Cadar, and A. Roychoudhury, “Agentic Concolic Execution,” in Proceedings of the IEEE Symposium on Security and Privacy (S&P), 2026, pp. 1673–1691. [51] H. Tu, S. Lee, Y. Li, P. Chen, L. Jiang, and M. Böhme, “Cottontail: Large Language Model-Driven Concolic Execution for Highly Structured Test Input Generation,” in Proceedings of the IEEE Symposium on Security and Privacy (S&P), 2026, pp. 3509–3527. [52] R. Feng, V. Gupta, V. Patel, V. R. Ernampati, and S. Saha, “Can Large Language Models Simulate Symbolic Execution Output Like KLEE?” arXiv preprint arXiv:2511.08530, 2025. [53] Y. Li, R. Meng, and G. J. Duck, “Large language model powered symbolic execution,” Proc. ACM Program. Lang., vol. 9, no. OOPSLA2, 2025. [54] Z. Li, S. Dutta, and M. Naik, “IRIS: LLM-assisted static analysis for detecting security vulnerabilities,” in International Conference on Learning Representations (ICLR), 2025, arXiv:2405.17238. [Online]. Available: https://arxiv.org/abs/2405.17238 [55] Y. Sun, J. Liu, D. Kroening, and J. Xue, “Agentic model checking,” arXiv:2605.21434, 2026. [Online]. Available: https://arxiv.org/abs/2605. 21434 [56] J. Guo, C. Wang, X. Xu, Z. Su, and X. Zhang, “RepoAudit: An Autonomous LLM-Agent for Repository-Level Code Auditing,” in Proceedings of the International Conference on Machine Learning (ICML), 2025. [57] Big Sleep team, “From Naptime to Big Sleep: Using Large Language Models To Catch Vulnerabilities In Real-World Code,” Google Project Zero Blog, November 2024. [Online]. Available: https://projectzero.google/2024/10/from-naptime-to-big-sleep.html [58] Y. Zhu, A. Kellermann, A. Gupta, P. Li, R. Fang, R. Bindu, and D. Kang, “Teams of LLM Agents can Exploit Zero-Day Vulnerabilities,” in Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), 2026, pp. 23–35. [59] R. Fang, R. Bindu, A. Gupta, and D. Kang, “LLM Agents can Autonomously Exploit One-day Vulnerabilities,” arXiv preprint arXiv:2404.08144, 2024. [60] S. Padmanabhuni, B. Karuturi, J. K. Indupalli, S. R. Chilla, and V. Yelleti, “Meta-Agentic Framework for Software Bug Detection using

Large Language Models,” in 2026 18th International Conference on COMmunication Systems and NETworks (COMSNETS). IEEE, 2026, pp. 841–846. [61] H. Li, Y. Hao, Y. Zhai, and Z. Qian, “Enhancing static analysis for practical bug detection: An LLM-integrated approach,” Proc. ACM Program. Lang., vol. 8, no. OOPSLA1, pp. 474–499, 2024. [62] H. Li, H. Zhang, K. Pei, and Z. Qian, “Towards more accurate static analysis for taint-style bug detection in Linux kernel,” in IEEE/ACM International Conference on Automated Software Engineering (ASE), 2025, pp. 380–392, arXiv:2504.11711. [Online]. Available: https://arxiv.org/abs/2504.11711 [63] X. Du, J. Feng, Y. Zou, W. Xu, J. Ma, W. Zhang, S. Liu, X. Peng, and Y. Lou, “Reducing false positives in static bug detection with LLMs: An empirical study in industry,” in International Conference on Software Engineering, Software Engineering in Practice (ICSE-SEIP), 2026, arXiv:2601.18844. [Online]. Available: https://arxiv.org/abs/2601.18844 [64] N. Mündler, M. N. Müller, J. He, and M. Vechev, “SWT-Bench: Testing and validating real-world bug-fixes with code agents,” in Advances in Neural Information Processing Systems (NeurIPS), 2024, arXiv:2406.12952. [Online]. Available: https://arxiv.org/abs/2406.12952 [65] Z. Zhao, C. Yang, W. Wang, Y. Yang, Z. Zhang, and L. Zhang, “AnyPoC: Universal proof-of-concept test generation for scalable LLM-based bug detection,” arXiv:2604.11950, 2026. [Online]. Available: https://arxiv.org/abs/2604.11950

Related documents

• Bug Finding With Agentic Symbolic Execution#1659178
• Understanding Bugs in Modern Agentic Frameworks: A Study of Symptoms, Root Causes, and Triggering Conditions#1199790
• A Neuro-Symbolic Reasoning Engine for Compilation-Free Patch Presence Testing#1411847
• From Runnable to Shippable: Multi-Agent Test-Driven Development for Generating Full-Stack Web Applications from Requirements#1011104
• Active-SWE: Benchmarking Coding Agents for Proactive Bug Fixing without Issue Reports#429420