Machine referee changes code agent work by raising verification cost
SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work
Software EngineeringLogic in Computer Science
Summary
This paper studies how having a machine judge, or referee, influences the way a computer program writes code. The referee can be a proof checker or a test set that decides if the program's work is correct, with no argument possible. The authors created a strict test protocol to measure exactly how much extra effort is needed when an agent must prove its code correct as judged by this referee. They found verifying the code adds a measurable cost in time or effort, but it varies by component size. This helps understand the trade-offs when requiring machine verification in software.
What this means in practice
- •For software developers: Estimate the extra time and effort needed to produce formally verified code under machine referee conditions for critical software components.
- •For software testing teams: Use the SaltBench protocol to fairly compare the impact of automated refutation tools on developer workflows isolated from external influence.
Authors
Jason Hickey
Abstract
SaltBench is a benchmark protocol for one question: How does a machine referee change the way a coding agent works? A machine referee --- a proof kernel, a program verifier, or a withheld test suite --- decides what an agent's work is worth, and the agent cannot argue with it. Here we report a protocol that makes the referee's effect measurable and whose answers cannot be narrated afterwards: every outcome is decided outside the agent's own toolchain; the agent is walled off from the network, the reference solutions and the harness itself, and the wall is tested by probes that try to breach it before any scored run, so the isolation is observed rather than assumed; every run is authorized by a dated freeze with its predictions registered; and a budget stop is a halt, never a failure. In this study, the subject of the benchmark is a ``seat'', meaning an agent session in its standard harness. We tested five systems components, all authored in Rust under a pinned Verus toolchain, with a withheld test suite as the referee for each. Four arms are tested: a plain agent; an agent that is also instructed to create a specification and verify the code against it, in a reduced rendering of the method, as registered; and two arms where the specification is provided a priori, extended under a dated amendment to $k=4$, where the registered sign test reached no verdict (3 of 4, $p = 0.3125$, every premium below the resolvable floor). We found that the arm instructed to specify and verify cost more on all five components, and by a practical margin: across these five components no premium exceeded $2.8879\times$ under either reading of the declared set, and the three cheapest sat below $1.4\times$. That bound is a property of this population and not a promise about larger ones: the premium runs near $1$ on the smallest components and rises with size. We publish the complete record.