When Fixed-n Eval Intervals Lie: A Verified Anytime-Valid Alternative for Post-Training Evaluation

Post-training loops evaluate adaptively: a running metric is watched across checkpoints and the run stops when the result looks decisive, or the best of several prompts, checkpoints, or reward models is reported. A benchmark score, however, is usually reported as a mean over a fixed number of items with a fixed-n confidence interval, and under adaptive reporting that interval loses its coverage guarantee: the headline number is less certain than its error bar claims. We quantify that gap and supply a remedy whose guarantee is machine-checked. The remedy is an empirical-Bernstein confidence sequence: an interval valid simultaneously at every sample size, so it holds under optional stopping directly and under selection with a union correction. Its coverage boundary is the same object a Lean 4 theorem certifies, so the bound under test is the bound the proof guarantees, not a reimplemented variant. On synthetic bounded scores, three fixed-n methods (Wald, item bootstrap, naive peeked) miscover by up to 29.3x the nominal alpha under peeking and by 3.6x to 6.4x under best-of-m selection; the confidence sequence holds at or below alpha in every adaptive cell. On real per-item correctness traces from a public benchmark dump (16 released models, no inference) the breach replicates: up to 24.9x under peeking, mild over the heterogeneous candidate set (1.1x to 2.1x) and growing over a near-tie cluster (up to 2.8x); the confidence sequence holds throughout. The contribution is narrow: a checkable boundary between a reported interval that retains its coverage under adaptive reporting and one that does not, verified in Lean. The price is stated plainly: 1.7x to 3.4x width, near-vacuous at the smallest stopping sizes.