§ Formal verification

Proof, where proof is possible.

A statistical library is a poor fit for testing alone: the interesting failures are index arithmetic, float edge cases, and structural invariants that only break on inputs nobody thinks to write down. Kani model-checks these over every input in a bounded space.

Kani proof harnesses

Files under proof

Unsafe blocks

Why model checking

A unit test tells you the function was right for the inputs you thought of. A bounded model checker tells you it is right for every input in a bounded space — or hands you the counterexample. For numeric code, where the failures live in index arithmetic and float edge cases nobody writes a test for, that difference is the whole argument.

Everything inside the dashed box is proven — every input, not a sample of them. The dots continuing past it are what the bound does not reach. Naming that edge is the difference between a proof and a claim.

Harnesses live in `#[cfg(kani)] mod verification` blocks co-located with the code they constrain, so they are invisible to normal builds and cost nothing at runtime.
Miri runs as the dynamic undefined-behaviour backstop for what Kani cannot reach.
Numerics are separately validated against `scipy.stats`, `scikit-learn`, `ruptures`, and `mlxtend` via committed golden fixtures, to documented tolerances between 1e-8 and 1e-12.
Sampling is deterministic, within a boundary worth stating precisely: a hand-written SplitMix64 gives a byte-identical uniform stream on every target, but anything downstream of a transcendental is not portable. Box–Muller calls `ln`, `sin`, and `cos`, which Rust delegates to the platform math library — sub-ULP accurate, not correctly rounded — and roughly 16% of normal draws differ by 1–2 ULP between architectures. So the uniform stream is pinned bit-for-bit and everything past it is checked to a tolerance derived from the standard error.
The full suite takes upwards of twenty minutes, so it runs as a release gate rather than on every push.

Selected harnesses

Names are quoted verbatim from the source. Filter by area, hover a name for the bounded space it is checked over, and click to copy it.

Resampling · Kani harness
A permutation resampler emits each index exactly once — it permutes rather than merely shuffling.
Checked over N = 4. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
ResamplingN = 4
A permutation resampler emits each index exactly once — it permutes rather than merely shuffling.
Resampling · Kani harness
K-fold test sets partition the dataset: no sample is held out twice, none is silently dropped.
Checked over N = 4, k = 2. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
ResamplingN = 4, k = 2
K-fold test sets partition the dataset: no sample is held out twice, none is silently dropped.
Resampling · Kani harness
Every bootstrap draw indexes inside the sample, for all sample sizes.
Checked over N = 3, B = 2. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
ResamplingN = 3, B = 2
Every bootstrap draw indexes inside the sample, for all sample sizes.
Resampling · Kani harness
Leave-one-out splits cover the dataset exactly once each.
Checked over n = 3. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
Resamplingn = 3
Leave-one-out splits cover the dataset exactly once each.
Streaming · Kani harness
Welford's streaming update can never yield a negative variance, whatever the input sequence.
Bound not published for this harness.
Streaming
Welford's streaming update can never yield a negative variance, whatever the input sequence.
Streaming · Kani harness
The P² quantile estimator's marker positions stay strictly ordered — the invariant the algorithm rests on.
Bound not published for this harness.
Streaming
The P² quantile estimator's marker positions stay strictly ordered — the invariant the algorithm rests on.
PRNG · Kani harness
Generated floats land in [0, 1) with no boundary escape.
Checked over exhaustive over u64. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
PRNGexhaustive over u64
Generated floats land in [0, 1) with no boundary escape.
PRNG · Kani harness
The integer-to-float conversion rounds faithfully rather than drifting at the extremes.
Checked over exhaustive over u64. CBMC is a bounded model checker — scalar domains are exhaustive, but size-parameterised properties are proven at small fixed sizes.
PRNGexhaustive over u64
The integer-to-float conversion rounds faithfully rather than drifting at the extremes.
Sampling · Kani harness
The ziggurat sampler's table lookups stay in range for every generated candidate.
Bound not published for this harness.
Sampling
The ziggurat sampler's table lookups stay in range for every generated candidate.
Algorithms · Kani harness
Classification argmax returns a valid class index, including for degenerate score vectors.
Bound not published for this harness.
Algorithms
Classification argmax returns a valid class index, including for degenerate score vectors.
Optimizers · Kani harness
Optimizer norms stay finite and non-negative — no NaN propagation into a descent step.
Bound not published for this harness.
Optimizers
Optimizer norms stay finite and non-negative — no NaN propagation into a descent step.
Distributions · Kani harness
The normal density is total: no input panics, including subnormals and infinities.
Bound not published for this harness.
Distributions
The normal density is total: no input panics, including subnormals and infinities.

Showing 12 of 12 named harnesses. Hover a name for its bound; click to copy it.

What a harness looks like

Quoted verbatim, doc comments included — that is where the reasoning for each bound lives, and it is the part worth reading. Every one of these carves through to the published crate, so it can be checked rather than taken on trust.

resampling_permutation_is_bijectionN = 4verbatim

A permutation resampler emits each index exactly once — it permutes rather than merely shuffling.

resampling/schemes.rs — rust
/// Proves [`permutation`] returns a genuine bijection of `0..N` for *every*
/// generator state: length `N`, every element in `0..N`, and each index
/// appearing exactly once. The Fisher–Yates swaps draw `j = uniform_index(i+1)`
/// with `j <= i < N`, so every `swap(i, j)` is in bounds — Kani discharges the
/// slice-access safety while the `seen` tally proves no index is dropped or
/// duplicated. `N = 4` keeps the three symbolic swaps tractable.
#[kani::proof]
#[kani::unwind(8)]
fn resampling_permutation_is_bijection() {
    const N: usize = 4;
    let state: u64 = kani::any();
    let mut rng = SplitMix64::new(state);
    let perm = permutation(N, &mut rng);
    assert!(perm.len() == N, "permutation length changed from {N}");
    let mut seen = [false; N];
    for &v in &perm {
        assert!(v < N, "permutation produced an out-of-range index {v}");
        assert!(!seen[v], "permutation repeated index {v}");
        seen[v] = true;
    }
    assert!(seen.iter().all(|&s| s), "permutation dropped an index");
}

in practice

In practice

Kani proof harnesses over the numeric kernels of a statistical computing library — index bounds, totality, structural invariants like bijectivity and partitioning.
Miri as the dynamic undefined-behaviour backstop for what model checking cannot reach.
Quality gates that lock invariants mechanically rather than by convention: a test that requires a written SAFETY justification for any future `unsafe`, in a codebase that currently contains none.
Reading and tracking the wider ecosystem — Creusot, Verus, Charon, Aeneas, Dafny, and the verified Rust standard library effort.

The suite lives in the yee-claw workspace; 68 of the 72 harnesses carve through to the published stats-claw crate, where they are checkable.

stats-claw