Where testing stops being enough
Property-based testing is the right default for numerical code. Generate thousands of inputs, assert invariants, shrink failures to a minimal case. It finds real bugs cheaply and it scales with almost no thought.
It is also a sampling technique. It tells you a property held on the inputs it tried. For most software that is sufficient, because the cost of a rare wrong answer is a bug report. For a small class of code (a numerical kernel other results are derived from, an allocation algorithm that must not be predictable, or a transform in a regulated pipeline), the cost of a rare wrong answer is that everything downstream is quietly wrong too, and nobody finds out for a year.
That is the boundary. Not "important code", which is everything. Code where being wrong is hard to detect from the outside.
Two tools, two jobs
The useful split is between proving the mathematics and enforcing the implementation.
Lean 4 proves the theorem. It operates on mathematical objects (the actual integers, the actual reals) with no representation limits. You state a property, and the proof either closes or it does not. There is no sampling and no flakiness.
Rust enforces the boundary. The type system cannot express "this converges", but it can express, at compile time, that a value was range-checked, that an invariant type cannot be constructed from unvalidated input, and that the unsafe numeric edges are confined to functions you can enumerate.
// The proof says the algorithm is correct for all real inputs.
// The type says this f64 was actually checked before we got here.
pub struct Finite(f64);
impl Finite {
pub fn new(x: f64) -> Option<Finite> {
if x.is_finite() { Some(Finite(x)) } else { None }
}
}
// Cannot be called with NaN or infinity. Not by convention - by construction.
pub fn newton_step(x: Finite, fx: Finite, dfx: NonZeroFinite) -> Finite { /* ... */ }
Neither tool covers the other's ground. A Lean proof about the reals says nothing about what your f64 does at the boundary, because f64 is not the reals; it is a finite approximation with its own arithmetic, where addition is not associative. A Rust type system says nothing about whether your iteration converges.
The gap everyone underestimates
This is where verification efforts actually fail, and it is not in either tool.
You prove a theorem about real-valued Newton iteration. You implement it in floating point. The proof is valid. The implementation is a different algorithm operating on a different number system, and the proof does not transfer. It constrains the design and rules out whole families of mistakes, but it does not certify the binary.
Closing that gap honestly means stating what was proved about what. "Convergence proven for exact arithmetic; floating-point error bounded empirically at 1e-12 over the tested domain" is a true and useful claim. "Formally verified" is neither, and it is the claim that gets made.
What a proof buys that a test does not
- Quantification. "For all n" instead of "for the 10,000 values of n we tried." The difference matters exactly when the counterexample is rare and structured, which is when property testing is weakest.
- Non-rot. A proof that still compiles still holds. A test suite can pass while asserting something that stopped being true; this is the silent-success failure mode in a different costume.
- Forced precision. Most of the value arrives before the proof closes. Stating the theorem exactly enough for a proof assistant surfaces the unstated assumptions, and those are usually where the bug was.
When not to do this
Proof effort is superlinear in specification complexity. A property about number theory closes in an afternoon; the same rigour applied to a stateful system with I/O is a research project.
Reach for proofs when the specification is small and the consequences of being wrong are large and hard to observe. Everywhere else, property-based testing plus a type system that makes illegal states unrepresentable gets most of the benefit for a fraction of the cost, and, unlike a proof, your colleagues can modify it.
UALBF pairs Lean 4 proofs with Rust and C implementations across a number-theoretic problem; OxidizeMath covers compiling verified numerics to WebAssembly without losing the guarantees at the boundary; Polyglot TSP benchmarks the same algorithm across toolchains, which is how you find out what the abstraction actually cost.