A fast number you cannot trust is a liability in a scientific pipeline. Derivon runs the same derivative tower in three registers: differentiable (for training), rigorous (outward-rounded interval and Taylor-model arithmetic), and formal (a Mathlib-free Lean 4 kernel that re-checks a finite obligation).
Enclosures, not point estimates
The rigorous core returns intervals that provably contain the true value. A certified divergence or robustness margin comes back as [lo, hi], never a bare float. Every enclosure is validated to contain both a dense deterministic grid and a random sample of true values.
from omnibias.core.verified.information import kl_divergence_enclosure
iv = kl_divergence_enclosure(p, q) # provably contains KL(p‖q)
print(iv.lo, iv.hi) # lo <= KL(p||q) <= hi, rigorously
Tamper-evident certificates
Results are sealed into a hash-stamped certificate format. An edited payload fails its own digest check, and an independent re-implementation ("the twin") regenerates the result with a different algorithm so a forged number fails replay.
The formal gate
For finite, rational obligations - a spectral ratio below one, a sign of an enclosed quantity, an error bound below a threshold - a bridge emits Lean that chains the kernel's proven soundness lemmas and runs lake build. The theorem_prover_verified flag is set only on a genuine kernel pass; it can never be forged by the certificate.
What this gives you is reproducible, falsifiable evidence with a precise, machine-checked statement of exactly what was verified - and an honest enumeration of what remains an open obligation.
Honest boundaries
We are deliberate about scope. The formal kernel discharges finite numerical inequalities; it does not formalize an analytic PDE theorem, and it never manufactures a grand claim. That honesty is a feature: it is what makes a certificate worth attaching to a regulated or safety-critical workflow.