New benchmark measures how code verification affects AI agent performance

Researchers have introduced SaltBench, an experimental framework designed to measure how machine-checked verification changes the behavior and output of AI coding agents. The work isolates the agent from network access, reference solutions, and external tooling while using a withheld test suite as an independent referee.

The Core Method#

The protocol employs several controls to ensure clean measurement. A wall between the agent and the test environment prevents contamination before evaluation runs. A dated freeze of predictions authorizes each test. Crucially, a token budget acts as a hard stop—runs that exceed the budget simply halt rather than fail, avoiding the agent gaming the completion metric.

The experiment tested five Rust systems components using a fixed version of the Verus toolchain. Each component was evaluated under three conditions: plain coding (baseline), salt-diet (agents instructed to both specify and verify their code), and two arms provided with specifications upfront.

Key Findings#

Verification came with a measurable cost. The salt-diet approach consistently required more tokens across all five components, with overheads ranging up to 2.8879× under different cost models. The three cheapest components stayed under 1.4× overhead. Smaller components showed near-parity costs, while larger ones saw the premium rise more steeply.

The full dataset covers 200 conditions across four language models, with 181 producing results of record. Of 497 total evaluations measured for correctness, 447 passed the withheld suite, 40 failed, and the remainder were censored or unscorable. The researchers note this is descriptive analysis without statistical verdict on whether verification improves code quality overall.

The complete data is publicly available, making the methodology transparent and the results open to scrutiny by the research community.