SaltBench asks how a machine referee (a proof kernel, program verifier or withheld test suite) changes how a coding agent works. Outcomes are decided outside the agent's toolchain; a wall probed before any scored run isolates the agent from the network, reference solutions and harness; a dated freeze of predictions authorizes each run; a budget stop is a halt, never a failure. Five Rust systems components on a pinned Verus toolchain are each refereed by a withheld test suite. The arms: plain; salt-diet, also instructed to specify and verify its code (a registered reduced rendering of the method); and two arms handed the specification a priori, where the registered sign test at k=4 reached no verdict (3 of 4, p = 0.3125). salt-diet cost more on all five components, by a practical margin: no premium exceeded 2.8879x under either reading of the declared set and the three cheapest sat below 1.4x, a bound of this population and not a promise about larger ones: the premium is near 1 on the smallest components and rises with size. Versions 2 and 3 add the complete pilot matrix: 200 conditions over four models, 181 with a result of record, 16 inexpressible and 3 declared unreached at the cost cap, costed in tokens, dollars and wall time, with no verdict on the arms. Version 3 adds a correctness reading, declared post hoc and registered after every verdict it reads existed and many had been read by its author: 447 cells pass the withheld suite, 40 fail, 10 are censored at a registered budget, 4 are unscorable and 42 are read by condition. salt-diet's pass-rate interval lies wholly below plain's on 8 greenfield and 5 brownfield rows and wholly above it on 2 greenfield rows. It is descriptive, over three cells of record per condition, with no test, and says nothing about whether the method makes code more or less correct. The full record is public.

翻译：暂无翻译