Agent automatically builds test setups to catch software bugs
Towards Agentic Proof Harness Engineering
Software Engineering
Summary
Checking if software works correctly often requires experts to create special test environments called proof harnesses, which take a lot of manual work. The authors developed an automated agent that builds these proof harnesses by analyzing a software project and its components. They tested this approach on real software and showed that the agent helped find three known bugs successfully. This method could save time and effort in making software more reliable by automating a tricky part of the verification process.
What this means in practice
- •For software verification engineers: Automatically generate proof harnesses to detect bugs during software verification of complex projects.
- •For software testers: Reuse automatically created test environments to apply different verification tools more efficiently.
Authors
Rohith Kumar Shanmuganathan, Cedric Richter, Heike Wehrheim
Abstract
Formal verification of real-world projects requires substantial manual effort, from specifying correctness properties to constructing the infrastructure needed to check them. We envision verification agents that assist developers throughout this process. Among the many tasks involved, one stands out as both foundational and amenable to automation: proof-harness engineering. A proof harness defines an isolated verification environment for a program unit, such as a function or module, by providing symbolic inputs, initialization code, and models of its dependencies. Today, proof-harness engineering remains largely a manual task performed by verification engineers. To explore the potential of coding agents for this task, we propose an agentic proof-harness engineer that automatically constructs verifier-ready harnesses from a software project and a designated verification target. We combine the agent with formal soundness and precision guards to validate generated abstractions and guide their refinement. We evaluate the feasibility of our approach in an exploratory case study on curl and libuv, using three historical assertion violations already embedded in the source code as verification properties. Our results show that the agent successfully constructs proof harnesses that enable CBMC to detect all three violations. We further demonstrate the potential for reusing these harnesses with other verification tools.