Symbolic execution stops stalling on environment setup: an AI agent supplies the database model, lifting CrossHair's executable functions from 4.5% to 81%
CrossHair, a symbolic execution tool, barely runs on real Python web applications because the code ships without contracts and its database calls cannot be executed symbolically. A pipeline pairing an AI coding agent with CrossHair automatically writes contracts for functions and synthesizes a symbolic model of the database, raising the share of executable functions from 4.5% to 81% across 11 open-source applications and 1,156,044 lines of code, and finding 221 bugs reproduced by tests. These bugs are mostly input-domain corner cases, and some are missed by direct inspection with the same model.