Does proof beat fuzzing? Testing Chelis on FPBench

Fuzzing is an automated software testing method that runs a program on many random inputs and checks that nothing goes wrong. It is cheap, fast and surprisingly good at finding bugs, so any proof tool (a tool that shows by mathematical reasoning, rather than by running the code, that a program meets its specification) has to prove its worth by finding bugs that fuzzing misses. We wanted to know whether Chelis' proof stack does that, so we tested it on FPBench, a standard suite of numerical kernels, i.e. small floating-point formulas from physics, control and math.

Chelis catches wrong answers that random testing almost never reaches, the type of bugs that usually get through a test suite and into production. To show this, we planted bugs in FPBench's kernels and counted how many each approach caught. Chelis' proof mode caught 74% of planted bugs, against the 42% caught by fuzzing. Even when we gave fuzzing 100,000 samples per invariant, proof mode caught 27 bugs that fuzzing missed altogether, every one of them a wrong answer confined to a narrow band inside the input range. Moreover, the narrower the band a bug hides in, the more proof adds!

How Chelis checks an invariant

In Chelis you state invariants, i.e. properties about a function that should always hold, such as "the result is never negative" or "the output grows with x", and chelis prove checks them. To achieve this, Chelis uses 1) a type checker that rejects code whose tensor shapes or numeric precisions do not line up, before anything runs, 2) an SMT solver that reasons about every input at once, and either proves an invariant or finds an input that breaks it, and 3) a sampler that runs the compiled code on many inputs, much like a fuzzer. Proof mode (auto) uses all three; fuzz-only skips the solver.

Because auto ends with the same sampler, anything fuzz-only finds, auto finds too. So the real question is simple: how much does the solver add on top of a fuzzer with the same budget?

The setup

We translated 103 FPBench kernels into Chelis and had LLMs write invariants for each one, such as bounds, monotonicity and identities, keeping only those that hold on the original code. Then we looked at two kinds of bug:

• Planted bugs are small edits we made so that a kernel goes wrong on only a sliver of its inputs. Most return a wrong result inside a narrow band, about 0.1% of one input's range. The rest clamp an input just inside its allowed range, which looks like ordinary input sanitizing.
• Natural defects are the ones FPBench's kernels already have: inputs their own preconditions allow where they return NaN or infinity, or lose accuracy to rounding.

A mode gets credit for a bug when it produces an input where an invariant fails. The details are in the last section.

What the solver adds

Here are both modes at Chelis' default of 100 samples per invariant. Each row shows the share of bugs each mode caught; the gap between the two dots is what the solver adds.

• The gap lives inside the input range. Nearly all of proof's 181 extra catches are wrong-result bugs there, where proof catches 65% against fuzzing's 16%. A hundred random samples rarely land in a band 0.1% wide. The solver does not need to land there: it reasons about all inputs at once and solves for one that breaks an invariant.
• At the edges it is a tie. The sampler deliberately tries boundary and extreme values, which is exactly where a clamp shows up.
• Proof pays off where the solver can handle the math. For some kernels the formula is beyond what the solver can reason about, and auto then falls back on the sampler. On the kernels it can handle, proof catches 83% against 37%; on the rest, 57% against 50%.

What about more samples?

A fair objection is that fuzzing only loses because 100 samples is too few. So we gave both modes a thousand times more.

With 100,000 samples, fuzzing alone catches 89% of planted bugs, against proof's 93%. Proof still catches 27 bugs that fuzzing misses, every one a wrong answer in a narrow band inside the input range. The gap narrows, but fuzzing at 100,000 samples took about 128 times as long as at 100 samples, and about 14 times as long as proof mode at 100 samples: roughly 17 hours of prover time against 71 minutes.

The narrower the band, the bigger the lead

To see how far this goes, we made the band each wrong-result bug hides in wider and narrower, from 1% of an input's range down to 0.001%.

The solver hardly cares about the width: it finds about 60% of these bugs however narrow the band gets. The fuzzer's share collapses, to 1% in the narrowest band. More samples help it only so far: at 10,000 samples it still finds just 14% of the bugs in the narrowest band, against 61% for proof.

FPBench's own defects

The planted bugs we already discussed are our own, but FPBench's kernels also come with real defects. Specifically, each kernel has a precondition, the range of inputs it promises to handle, and 26 of them return NaN or infinity for some input in that range, for example by dividing by zero. These defects are much easier to sample than our narrow bands, so the sampler finds most of them by itself. What proof adds here is reach!

• Proof finds three defects fuzzing does not as their preconditions use guards the sampler cannot generate inputs for, such as b*b >= 4*a*c, so it never runs the code at all. The solver handles the constraint directly and finds a real failing input, for example a = -2.8×10^-309, b = 1 and c = -9×10³⁰⁷ in the quadratic formula, where dividing by the tiny 2a overflows to infinity.

Conclusion

On numerical kernels, proof finds bugs that fuzzing misses, and the gap grows as bugs get harder to sample. The solver's contribution comes almost entirely from wrong answers hidden inside the input range. With a thousand times more samples, fuzzing closes much of the gap, but only by spending far more time than the solver does.

The result is clear: when a wrong answer hides somewhere random inputs rarely land, proof is what finds it.

The details

FPBench

FPBench is a community benchmark suite for floating-point analysis tools. It collects small numerical kernels from control, physics and mathematics, drawn from papers on floating-point accuracy and verification, and writes them all in one shared format, FPCore, so that different tools can be compared on the same programs. Every kernel comes with a precondition giving the inputs it is meant to handle, which suits this experiment: for each function we know exactly what a valid input is. The suite and its sources are on GitHub under the MIT license.

We translated the kernels from FPCore to Chelis with a deterministic translator, with no LLM involved, and checked every translation against an IEEE reference evaluator. 103 of FPBench's 130 kernels made it through: all 103 agree with the reference within 10^-12, and 93 agree bit for bit. The translator does not handle the other 27: 10 written for single precision, 9 that use loops, 3 that raise to a non-integer power, one with an annotated argument, one that uses acos, and 3 whose metadata it misread.

Invariants and bugs

For each kernel two LLMs (Claude Opus and Haiku) wrote invariants, and we kept only those that held on the original code. Both modes were checked against exactly this set, so the comparison between them is fair, but the absolute numbers depend on it. Stronger or weaker invariants would move both.

Each wrong-result bug makes the kernel 5% too large or too small, negated, or off by 0.01, inside a band about 0.1% wide along one input, placed at random. Each clamp bug clamps one input just inside its bound.

A detection counts only if it holds up: a mode gets credit when the invariant is shown to fail on the buggy code by evaluating it at a concrete input, and a planted bug is in the count only if at least one of its kernel's invariants actually fails on it. The solver "can handle" a kernel when, in a pilot run before the experiment, it could prove an invariant about that kernel on its own.

Beyond FPBench

We tried the same comparison on eight finance functions sampled from QFBench, a quantitative-finance benchmark, each implemented by a coding agent. The direction held, but the effect was smaller: at the default budget proof caught 34% against fuzzing's 25%, with 6 bugs caught only by proof (p = 0.031).

Limits

The kernels are short formulas from one suite, and larger programs with loops and data structures are untested. The invariants were written by LLMs, and better invariants would raise both modes.