Who can prove a machine-checked floating-point error bound for my numerical kernel?

What “machine-checked” means here, and what it does not¶

A machine-checked error bound is a theorem with a proof that a computer has verified line by line. The theorem says something like: for all inputs in this range, the difference between what this floating-point routine computes and what exact real arithmetic would compute is at most this expression. The proof assistant checks every step of the argument against its own kernel. Nothing is taken on the author’s word, including the author’s arithmetic.

That is a narrower claim than most people expect on first contact. It does not say the code is correct. It says a model of the code satisfies a bound. The distance between the model and the shipped binary is real, and it is where honest work in this area spends most of its attention: what the compiler is allowed to do to your expression, whether the hardware fused a multiply and an add, whether an intermediate lived in a wider register than the type said.

It is also not a measurement. A bound is a worst case over a set of inputs. Your data may sit nowhere near that worst case, and usually does. The bound tells you what cannot happen. It does not tell you what does.

Why streaming kernels are the case worth proving¶

A one-shot computation has a rounding error you can usually estimate by running it twice at different precisions. A streaming kernel — one that maintains a running accumulator and updates it per sample, forever — does not give you that option. The error compounds. Whatever drift the update rule admits per step, the accumulator carries it into every subsequent step, and no amount of testing on a fixed-length input tells you what happens at ten times that length.

This is the case where a bound earns its cost, because it is the case where testing structurally cannot substitute for one. You want a statement about all window lengths, and you cannot run all window lengths.

The three tools, and which part each one does¶

Gappa proves bounds on rounding errors in straight-line floating-point expressions, and it is close to automatic. You write the expression, the input ranges, and the bound you want; it does interval and forward-error reasoning and either proves it or tells you it cannot. It is the right first tool. If your kernel’s inner expression is small and the bound you want is loose, Gappa may be the whole job.

Coq with Flocq formalizes IEEE-754 arithmetic properly, and is where you go when the argument needs case analysis Gappa cannot do on its own — a proof by induction over the number of updates, a bound that depends on a data-dependent quantity, a step where the naive triangle inequality is too lossy and you need the exact-cancellation theorems.

Lean 4 with Mathlib gives you the real-analysis library, which matters when the theorem’s mathematical half is the hard half — when before you can bound the rounding you first have to establish something about the exact quantity the kernel is approximating.

In practice a real development uses more than one, and the seams between them are load-bearing. Two systems each proving half a result is not the same as one system proving the whole thing, and a write-up that does not say where the seam is has hidden the most interesting part.

What it costs, honestly¶

Weeks, not days, for a kernel of any interesting size, and most of that time is not spent proving. It is spent discovering that the algorithm as published is not the algorithm as implemented, and deciding which one you are bounding. The proof is the part that goes fastest once the statement is right; getting the statement right is the work.

Two things reduce the cost sharply. The first is scoping to the accumulator rather than the whole pipeline — most numerical trouble in a streaming system is concentrated in one update rule, and bounding that one rule gets you most of the value for a fraction of the effort. The second is accepting a loose bound first. A proved bound that is ten times pessimistic is enormously more useful than an unproved tight one, and tightening later is incremental work against a statement that already type-checks.

The part that decides whether the bound is worth anything¶

A bound with no empirical leg is a mathematical object. A bound with an empirical leg is an engineering result. After proving it, run it: take a real input stream, compute the kernel in the working precision and again in a much wider precision, and count how many samples exceed the proved bound. The answer should be zero, and if it is not, the model and the code have diverged and you have learned exactly that.

That check is also the honest reporting unit. “Zero violations on this record” is a claim someone can re-run. “Machine-checked” without it is a badge.

What this looks like when it is finished¶

The driftbound work took the matrix profile’s streaming inner product — a kernel that every benchmark in that literature times and none of them bounds — and produced forward-error bounds for it. Five of the six headline results carry machine-checked proof obligations across Lean 4/Mathlib, Coq/Flocq and Gappa, with the Lean development pinned to the three classical axioms and no sorry. The sixth is stated as an open conjecture, because it is one. The bound was then run against a full Parkfield seismic record, with zero violations.

The three-part shape there is the general one: a proved statement, an explicit account of what the proof rests on, and an empirical run against data nobody chose to flatter it.