Verified estimation gallery

7 filters — linear Kalman, matrix EKF, quaternion AHRS — each proven (Lean, sorryAx-free), simulated as a working filter on the real Forge-emitted kernels, and run on silicon (Verilog/Verilator bit-exact). One math source per kernel; no numpy in any estimator.

Scalar Kalman filter — proven optimal, on silicon at 100 MHz all checks pass

The flagship. A scalar Kalman filter carrying state across measurements (P ← P·r/(P+r) — a division in the feedback path), proven MMSE-optimal and fixed-point-error-bounded, running bit-exact and tracking at 100 MHz on a real Arty A7-100T.

emit

32 compiled targets

prove (Lean, sorryAx-free)

  • kalman_recursive_mmse ✓ clean — each recursive step's posterior mean is MMSE-optimal (conjugacy self-composition) axiom trail
  • kalman_variance_recursion_fixed_point ✓ clean — the Q16.16 variance recursion stays within a proven bound of the exact recursion over N steps axiom trail
  • kalman_estimate_recursion_coupled ✓ clean — the estimate recursion's fixed-point error is bounded — the gain error derived from the variance error axiom trail

simulate — the real emitted kernels

quantityresult
filter RMS vs measurement RMS0.071 / 0.325 ratio 0.22 < 1✓
estimate converges to truth|2.4812 − 2.5| = 0.0188 < 0.10✓
posterior variance shrinks1.000 → 0.01538 < 0.05✓

silicon

on a real Arty A7-100T at 100 MHz, whole-design — eml_reciprocal +1.102 ns, kalman_update_1d +0.587 ns, kalman_filter_step +0.866 ns. all three anchors close 100 MHz WHOLE-DESIGN (0 failing endpoints, DRC clean); 170 passes bit-exact to the golden recursion, the estimate tracks and P shrinks 1.0 → 0.015

full report →

Recursive 2-D Kalman filter — whole filter, 32 DSPs, 100 MHz on silicon all checks pass

The capstone: measurement update + Joseph covariance update, looped with (x,P) state feedback, all through shared MACs + one reciprocal. It tracks a target with the covariance shrinking, and the WHOLE recursive filter closes 100 MHz on a real Arty A7-100T in 32 DSP48s — 13% of the device, less than a third of what the unrolled measurement update alone cost. Scope (graded honestly): the two halves are machine-checked (forward-error bound + MMSE-optimality + Joseph PSD); the composition into 'implemented ≈ optimal' is ARGUED, not yet a Lean theorem; and the shared scheduler/control is verified BIT-EXACT (301 silicon frames, Verilator shared==unrolled), not proven.

emit

15 compiled targets

prove (Lean, sorryAx-free)

  • kalman2_state_update_fxerr ✓ clean — the fixed-point measurement update x'=x+K(z-x) is forward-error bounded through the inverse axiom trail
  • matrix2_posterior_mean_mmse ✓ clean — the posterior-mean estimate is MMSE-optimal (trace loss, per-component) axiom trail
  • kalman2_joseph_psd ✓ clean — the Joseph covariance step keeps P symmetric PSD for any gain — so recursing it is safe axiom trail

simulate — the real emitted kernels

quantityresult
estimate converges to target|err| = 0.0532 < 0.10✓
covariance trace shrinks monotonically0.4000 → 0.0244 monotone ↓ yes✓
final trace(P) vs initial0.0244 / 0.4000 < 0.1000✓

silicon

on a real Arty A7-100T at 100 MHz, whole-design — kalman2d_filter +0.715 ns. 32 DSP48s for the WHOLE recursive filter (24 reciprocal + two shared MACs) = 13% of the device, vs 100 for the unrolled measurement update ALONE; 8/8 trajectory steps bit-exact, 247 cycles/step, trace(P) 0.39 → 0.06.

full report →

Joseph covariance update — PSD for any gain, 4 DSPs on silicon all checks pass

The numerically-robust covariance step P+ = (I-K)P(I-K)^T + K R K^T — four 2x2 matrix products — time-multiplexed through ONE shared MAC. Proven to stay PSD for any gain (so recursing it is safe), and the whole four-product update costs 4 DSP48s on real fabric at 100 MHz (vs ~128 unrolled).

emit

14 compiled targets

prove (Lean, sorryAx-free)

  • kalman2_joseph_psd ✓ clean — P+ = (I-K)P(I-K)^T + K R K^T stays symmetric positive-semidefinite for ANY gain K axiom trail
  • fxerr_dot2_fullwidth ✓ clean — the full-width scheduled dot's forward error is a single rounding (<= 2^-FRAC per dot) axiom trail

simulate — the real emitted kernels

quantityresult
P+ stays PSD over 500 random (P,R,K)all PSD = PSD✓
P+ off-diagonal symmetry (max |P01-P10|)6.10e-05 < 1e-3✓

silicon

on a real Arty A7-100T at 100 MHz, whole-design — joseph2_update +1.350 ns. 4 DSP48s for the whole four-product update (vs ~128 unrolled); 6/6 cases bit-exact; closes 100 MHz after registering the shared operand mux.

full report →

Shared-MAC matrix multiply — flat DSP cost, on silicon all checks pass

A matrix multiply time-multiplexed through ONE shared multiplier instead of unrolling to N*K*P of them. Bit-identical to the unrolled matmul (so no separate proof — the win is structural and measured): on real fabric the whole product costs 4 DSP48s, and the SAME 4 for a 2x2 and a 3x3 — flat in matrix size.

emit

14 compiled targets

prove (Lean, sorryAx-free)

    simulate — the real emitted kernels

    quantityresult
    shared-MAC matmul vs exact real product (max cell error)2.01e-05 < 1e-3✓

    silicon

    on a real Arty A7-100T at 100 MHz, whole-design — matmul2_pipeline (2x2) +1.693 ns. 4 DSP48s for the 2x2 AND the 3x3 — flat in matrix size (vs ~32 / ~108 unrolled, an 8x / 27x collapse); 6/6 cases bit-exact over UART.

    full report →

    Linear Kalman tracker (constant velocity) all checks pass

    A textbook predict→update Kalman filter — cuts position noise and recovers the unmeasured velocity from position measurements alone.

    emit

    32 compiled targets

    prove (Lean, sorryAx-free)

    • kalman2d_cov_predict_psd ✓ clean — the predicted covariance F·P·Fᵀ+Q stays positive-semidefinite axiom trail
    • kalman2d_joseph_psd ✓ clean — the Joseph covariance update preserves PSD for any gain axiom trail

    simulate — the real emitted kernels

    quantityresult
    filter RMS vs measurement RMS0.525 / 0.934 ratio 0.56 < 0.6✓
    recovered velocity (never measured)0.516 ≈ 0.5✓
    max |filter − NumPy-KF|1.1e-16 < 1e-9✓

    silicon

    kalman2d_predict.cov_predict — Verilog/Verilator bit-exact

    full report →

    EKF localization (range-only, two beacons) all checks pass

    A nonlinear Extended Kalman Filter — range-only trilateration to two beacons; the gain K = P·Hᵀ·(H·P·Hᵀ+R)⁻¹ exercises the matrix-inverse operator.

    emit

    100 compiled targets

    prove (Lean, sorryAx-free)

    • ekf_range_nonneg ✓ clean — the range measurement √((lx-x)²+(ly-y)²) is ≥ 0 axiom trail
    • kalman2d_innovation_cov_psd ✓ clean — the innovation covariance H·P·Hᵀ+R stays positive-semidefinite axiom trail
    • kalman2d_matrix_joseph_psd ✓ clean — the Joseph covariance update A·P·Aᵀ+W preserves PSD for any gain axiom trail

    simulate — the real emitted kernels

    quantityresult
    EKF position RMSE vs dead-reckoning0.479 / 2.993 ratio 0.16 < 0.6✓
    max |EKF − NumPy-EKF|3.6e-15 < 1e-9✓

    silicon

    complementary_filter.fuse, weighted_fusion.fuse3, kalman2d_update_matrix.update_cov — Verilog/Verilator bit-exact

    full report →

    Mahony AHRS (quaternion attitude) all checks pass

    A complementary attitude filter fusing a biased gyroscope with an accelerometer; every quaternion op is a shipped kernel and the state is re-normalised onto the unit sphere each step.

    emit

    18 compiled targets

    prove (Lean, sorryAx-free)

    • quat_normalize_unit ✓ clean — ‖normalize(q)‖² = 1 — the state stays a unit quaternion (sorryAx-free) axiom trail

    simulate — the real emitted kernels

    quantityresult
    Mahony attitude error vs gyro-only2.38° / 18.44° ratio 0.13 < 0.3✓
    max |‖q‖ − 1| over the run2.2e-16 < 1e-12✓

    silicon

    quat_mul, quat_rotate_vec — Verilog/Verilator bit-exact

    full report →