Machine-checked theorems about compiled numerics.
MachLib — Lean 4, Mathlib-free, every trusted axiom listed and accounted for.
MachLib is a Lean 4 library that proves things about EML kernels: the small exp/log expression language that Forge compiles to C, GPU code and RTL. It carries its own axiomatised reals instead of Mathlib, so the compiler's proof obligations build in a minute — and every axiom its headline theorems rest on is accounted for: witnessed in Mathlib by a sibling project, interpreted, or, for the IEEE-754 floor, measured.
Measured, with the command that reproduces each one.
Every figure here is the output of a command run on 2026-09-15, and a gate in the repository fails if the text drifts from the corpus. Re-run the command before quoting a number; the README lists them.
Live build status: fetching…
What it proves.
Everything named here is free of sorry and of any classical Khovanskii axiom; #print axioms confirms it. The general-depth Khovanskii bound is still cited, not proved, and is kept out of every featured result.
Verified numerics
From bits toward trajectories, for the kernels Forge emits.
fxaffine_traj_tracks_exact— The bit-level fixed-point datapath of the affine plant kernel tracks the exact real trajectory within ulp · geom c n, with the per-step error derived from the bits. This is the end-to-end result for a plant with no controller state.spiloop_tracks_exact— The same join with an integrator: a signed bit-level PI closed loop tracks the exact real PI trajectory within 4 ulp · geom L n plus transient. It is general rather than a worked example, because a PI loop's integrator row forces its left eigenvectors and the resulting eigen equations are ring identities. A companion theorem covers under-damped designs, whose eigenvalues are complex and admit no real eigenvector, so every PI design is covered whatever its damping. The derivative term is joined at the datapath too (spidloop_tracks_exact): in a PID loop the integrator row is exact and the delay row is a wire, so every rounding error comes from the state row's three multiplies. Under-damped designs, whose eigenvalues are complex, are covered by a squared measure that needs no square roots, so every PI and PID design is covered whatever its damping.cross_target— Two evaluations of one exact value at different precisions agree within their forward-error bounds.kalman_update_1d_fwd_error— A proven Q16.16 forward-error bound for the scalar Kalman update that ran on an Arty A7 and is the datapath of the second chip.nonlinear_drift_clamp_safe— A saturating guard keeps a plant's state inside a safe envelope for all time, under any controller signal and bounded disturbance.intModel— The flagship closure's axioms have an external ℤ-model, so those results are not vacuous. A gate fails if the model ever becomes circular.
The EML language itself
What finite exp/log depth can express, and how tame it is.
chain2_khovanskii_bound_explicit— A Khovanskii zero bound for depth-2 double-exponential chains (x, eˣ, e^{eˣ}) with the reducibility witness constructed, in an explicit numeric form usable as a tool.invX4_depth_optimal— The reciprocal is an EML tree on x > 0, and depth 4 is optimal — certified by a lower-bound theorem, not by a search.x_plus_neg_c_depth_exact_four— Translation by a constant costs depth exactly 4, both bounds proved.sign_query_cost_bounds_tight— The query-complexity lane: log is not a rational germ on any interval, and the sign function costs between 1 and 12 queries.depth3ApproachBelow_holds— The depth-3 constant-gap statement is false (a witness refutes it), and its decaying-floor replacement is proved: a depth-≤3 tree that dips below a constant does so by at least exp(−C − exp(exp x)).
Zero unaccounted axioms. Not zero axioms.
Everything Mathlib would prove as a theorem — the ordered field of reals, the definitions and derivatives of exp, log, sin and cos, the floating-point model — is an axiom here. A library built on axioms can be vacuous without a single sorry, so nothing inside MachLib is allowed to vouch for MachLib. A sibling project that imports both Mathlib and MachLib checks, in the kernel, that a Mathlib term inhabits the interpreted type of each witnessable axiom. The manifest listing all 169 is generated, and a gate fails if the witness project stops running — it did once, for 33 days.
The 32 float-bridge axioms are a different kind of trust and are not averaged in. A hardware certificate rests on exactly those; read that block of the manifest first.
Three ways in, each ending in a command.
Nothing on this page asks to be believed. GitHub's hosted runner times a cold build from a fresh clone on every push to master that touches the library; on 2026-09-15 two runs took 7 and 13 minutes. The full gate run took just under 20 minutes on a 20-core workstation.
Check it
Clone, build, and run every gate. The runner prints each verdict and exits non-zero if any gate fails, and it refuses to certify a tree that changed while it ran.
Read it
The claim inventory says what is proven, what it rests on and what is open, with a command next to each claim. If something there cannot be reproduced in a few commands, that is a bug in the document.
Reproduce it
The range-bearing EKF package holds everything a stranger needs to walk one kernel from source to certificate to silicon anchor. It exists because the first outside reproducer got two of five, and a reproduction claim that withholds its evidence is not one.
The seams, named.
- No claim about physical silicon beyond the reproduction package and the bench evidence it cites. A theorem about a datapath is a theorem about the datapath.
- No compiler-correctness claim for Forge. The certifier binds a proof to a kernel by hash; it does not verify code generation.
- The analytic base is axiomatised, not constructed. Every trusted axiom is listed and accounted for — witnessed in Mathlib, interpreted, or measured; none is proved here.
- The end-to-end composition from bits to a closed-loop trajectory is proved for the affine plant kernel, not yet for the PID controller path.
- The research lane on the EML language is the work of one author: kernel-checked, not yet externally reviewed.
- Counts are snapshots. Re-run the command before quoting one.
A partial result is committed by naming what it lacks. An open question is a proposition a theorem may consume and nothing may conclude, tracked in a ledger that fails the build in both directions: when a row says open after the corpus closed it, and when a row says discharged by a theorem that does not conclude it.
Every instrument here must be shown capable of both verdicts before either is read. A check that cannot fail is not a check.
One link in a chain that has to hold end to end.
Forge compiles a kernel and emits its proof obligations into this library; this library proves what it can and names what it cannot; a sibling project checks this library's own axioms against Mathlib. None of the three vouches for itself.