AI Coding Benchmarks Need Proofs, Not Just Tests

This paper argues that AI coding benchmarks need proof-based evaluation, not just passing tests. As frontier LLMs saturate test-based benchmarks, the signal they provide about code correctness degrades: a finite test suite cannot distinguish correct code from merely plausible code, and no finite curation effort can turn test passing into a general guarantee of semantic correctness. Proof-based evaluation, where each correctness claim is backed by a machine-checkable witness against an explicit formal specification, is the strongest practical oracle we know for moving beyond sampled behavioral checks. The window may be narrow: if benchmark targets shape training, then test-only leaderboards risk reinforcing code generation without corresponding proof-generation capability. Our argument rests on three planks: a structural argument that scaling tests cannot close the correctness gap, empirical evidence from two Lean~4 benchmarks under two frontier models, and a hand-formalized case-study grid drawn from SWE-Bench.