Formal verification of NIST SP 800-90B min-entropy estimators in Lean 4, built against mathlib4.
Companion to lopt, an entropy provisioning service. Theorems here are intended for eventual upstream contribution to mathlib where applicable.
| Estimator (NIST SP 800-90B §6) | Lean | Notes |
|---|---|---|
| §6.3.1 Most Common Value (MCV) | ✅ Complete, sorry-free |
LoptEntropy/Entropy/MCV.lean. Deterministic core fully proved; probabilistic wrapper takes the normal-approximation event as hypothesis pending a standard normal CDF in mathlib. |
| §6.3.2 Markov | — | Planned |
| §6.3.3 Compression | — | Planned |
| Composition (min of estimators ⇒ bound) | — | Planned, after the three estimators are individually formalized |
| Contribution | Lean | Notes |
|---|---|---|
StieltjesFunction.generalizedInverse (quantile function) |
✅ Complete, sorry-free |
LoptEntropy/Mathlib/StieltjesFunction/Inverse.lean. Galois-connection-based, with monotonicity, left-continuity, and inversion-on-strict-monotone-range. Intended for upstream contribution to mathlib's MeasureTheory.Measure.Stieltjes. Open design questions enumerated in the file footer; Zulip discussion in progress. |
The probabilistic wrapper of MCV currently axiomatizes the normal-
approximation event because mathlib does not yet provide a packaged
standard normal CDF Φ and its inverse Φ⁻¹. The path forward, per Lean
Zulip discussion with Etienne Marion, is to define the inverse on the
general StieltjesFunction first (now done — see prerequisite-work
table above), then instantiate for the Gaussian density to derive Φ⁻¹
as a corollary. The original Zulip thread is at
#mathlib4 → Standard normal CDF Φ — status in mathlib?.
lake buildPinned mathlib version is fixed in lake-manifest.json. CI on every
PR and push to trunk runs lake build; green means all theorems
compile clean against the pinned mathlib commit.
The MCV estimator is a runtime check in lopt's TRNG service. Its claim ("the empirical maximum-frequency bound, padded by a confidence margin, is a conservative lower bound on min-entropy") is one of the load-bearing audit-grade claims of that service. A formal Lean proof turns "the SP 800-90B reference implementation says so" into "the theorem is checked by Lean against mathlib."
This is the first slice of an entropy-chain formalization. The remaining estimators, the composition theorem, and the conditioning function's min-entropy preservation are the natural follow-ups.
Theorems that generalize beyond the lopt use case are intended for upstream contribution to mathlib. The plan, per Lean Zulip dialogue:
- Prototype here against pinned mathlib
- Discuss design on
#mathlib4(especially API and naming conventions) before opening a mathlib PR - Open the mathlib PR with the smallest possible scope, citing this repo as the originating context
Pull requests to this repo are welcome from anyone; PR review and merge authority rests with the Xylem Group maintainer line.
The Most Common Value formalization was produced by Harmonic's Aristotle, an automated theorem prover for Lean 4. Each contribution is reviewed by a human before merge. Future contributions may come from Aristotle, from mathlib community members, or from direct human work — the source is disclosed in the commit message of each PR.
Apache License 2.0 — see LICENSE.
Choice of Apache 2.0 (vs MIT or GPL) matches mathlib4's own license, keeps upstream contribution paths frictionless, and provides the explicit patent grant + termination clause appropriate for crypto-adjacent work.
If this work supports a paper, please cite as:
@misc{lopt-entropy-formal,
author = {Xylem Group},
title = {lopt-entropy-formal: Formal verification of NIST SP 800-90B estimators in Lean 4},
year = {2026},
howpublished = {\url{https://github.com/Xylem-Group/lopt-entropy-formal}},
}
Specific theorems should additionally cite the relevant Lean file
path (e.g. LoptEntropy/Entropy/MCV.lean).
- Harmonic's Aristotle — the theorem prover used to produce the initial MCV formalization
- NIST SP 800-90B (January 2018) — the source standard
- mathlib4 — the upstream Lean math library
- lopt — the consumer entropy-provisioning service that motivated this work