Symbolic execution stops stalling on environment setup: an AI agent supplies the database model, lifting CrossHair's executable functions from 4.5% to 81%

Symbolic execution now reaches a class of code it could previously hardly analyze: Python web applications that depend on a database. With no environment at all, CrossHair executes 243 of 5,406 contracted functions, or 4.5%; initializing the framework the way a project's own test suite does raises that to 1,595, or 29.5%. Across 11 open-source applications totaling 1,156,044 lines of Python, the synthesized environment lets CrossHair execute 4,394 functions, or 81%, with each repository between 66% and 89%.

The pipeline supplies the two inputs symbolic execution lacks: function contracts and a model of the external environment. Previously these stubs, lazy-initialization bounds and database models had to be written by hand for every project, which is why the techniques rarely reached large database applications. The agent works from framework knowledge packaged in skills and from repository inspection, generates schema-constrained ORM stubs and a bounded lazy-initialization plugin, installs them through CrossHair's plugin interface without modifying the engine, and repairs them until CrossHair can load them.

Every candidate bug must pass an audit and be reproduced by real execution before it counts. A counterexample from symbolic execution may come from an over-strong contract or an over-approximate environment and is not necessarily an application bug. The audit splits 2,113 refuted functions into 241 real bugs, 1,281 false positives, 562 tool artifacts and 29 failures located only inside an installed library; the pipeline reports 1,050 bugs reproduced by unit tests, 920 of them end-to-end on the running application.

The bugs symbolic execution finds differ in kind from those the same model finds by reading code, so the two are complementary. A baseline in which the same model inspects the code reproduces 1,824 bugs, more in total than the pipeline's 1,050. The pipeline finds 312 bugs the baseline misses, 73 of them found by CrossHair; CrossHair's bugs are mostly input-domain corner cases such as empty strings, missing fields and unusual characters, while the baseline's are mostly wrong-output bugs.

The demonstrated scope is 11 popular open-source Python web applications covering two ORMs, Django and SQLAlchemy, all run with a single frontier model in one harness. The authors explicitly do not argue that symbolic execution finds more or more important bugs than an LLM reading the code; they show that once an agent supplies the environment, it runs on large database-backed applications and finds the input-domain corner cases it is known for.

Contracts are synthesized by the agent, so an over-strong postcondition can manufacture a finding no developer would call a bug, while a postcondition that asserts too little raises no alarm; the bug counts are therefore a precision-oriented lower bound, not a recall measure. The reach ablation separates framework initialization from the synthesized environment as a whole but not the stubs, lazy initialization and framework stand-ins from one another, and one configuration per repository is reported without variance across repeated runs.