Formal Verification
Proven, not just tested.
Pricing libraries are easy to write and hard to verify. FerroRisk's mathematics is verified end-to-end, in layers — each doing what it can actually prove, with an explicit map of where each layer's reach ends. The pricing identities are machine-checked in the Lean theorem prover; the floating-point kernels carry rigorous rounding bounds in Gappa, re-checked by the Coq kernel. This is the assurance level of avionics and cryptography — applied to an options-analytics crate.
Greeks, parity, no-arb bounds, convexity, the Black-Scholes PDE, and implied-vol uniqueness — proven over the reals.
Every headline theorem reduces to propext, Classical.choice, and Quot.sound — the audit fails on any sorry or non-standard axiom.
The Jaeckel path converges to the target price at ~3e-16 in two iterations — no bisection fallback, no errors, across the wings.
The erfcx numerator is tight to ≤0.34 ulp, the normalised-Black assembly to ≤1 ulp — rounding bounds the Coq kernel re-verifies.
The Layers
Verified in layers, each doing what it can prove
There is no single "verified" checkbox. Different claims need different machinery — and the honest version says so explicitly.
| Layer | What it establishes | On what | Strength |
|---|---|---|---|
| Proven (ℝ) | The options-pricing mathematics is correct | An idealized ℝ model (Lean) | Lean-kernel-checked · minimal axioms · no sorry |
| Proven (structural) | Exposure / sign / netting logic is correct | The real shipping Rust (Aeneas) | Lean-kernel-checked |
| Measured (f64) | The proved relationships hold in the shipping code | The real code, on a 672-point grid | Validated to ~1e-15 |
| Bounded (f64) | The numeric kernels round / approximate correctly | The real code (Gappa + Sollya) | Rigorous upper bounds · Coq-checked |
What Each Layer Proves
From the reals down to the float
Proven over ℝ — the pricing mathematics
formal/lean-math/ — 310public theorems and lemmas in Lean + mathlib. The normal CDF is specified by its textbook properties, then discharged for the concrete Gaussian (nothing axiomatized): put-call parity, no-arb bounds, the BSM density identity, the complete first-order Greeks with signs, monotonicity in every parameter, convexity and calendar no-arbitrage, second-order Greeks (vanna, vomma, charm, the vega-gamma identity), the Black-Scholes PDE, implied-vol existence & uniqueness, Black-76, and Bachelier — plus the analytics laws layered on top: σ-standardized moneyness round-trip and monotonicity, the realized-semivariance sign partition and its exact recombination, the discrete-dividend escrow (PV non-negativity, spot domination, ex-time anti-monotonicity, and the theta / rho correction lemmas), and the early-exercise-premium fraction bound. This includes 47 American proofs over boundary admission, weighted derivatives and deterministic exercise, under their stated assumptions. These exact-model proofs do not verify the complete floating-point American implementation.
Proven on the real Rust — structural laws
The exposure / sign / netting law_* targets are proved directly on the Aeneas-generated translation of src/formal_model.rs — verification of the actual Rust, not a hand-written model of it. Scope is honest: this covers the integer plumbing; Aeneas has no floating-point model.
Measured in f64 — the proved laws, in the shipping code
tests/formal_conformance.rs checks each proved relationship in the real f64 pricing/Greek code over a 672-point grid (deep-ITM…OTM × short…long T × low…high vol × rates × dividends): parity 1e-15, the vega-gamma identity 1e-15, the PDE 2.1e-14, zero bounds/monotonicity violations, convexity to the finite-difference floor.
Bounded in f64 — the numeric kernels
The transcendental kernels carry two machine-checked error components. Rounding: formal/gappa/ proves the f64 evaluation matches exact-real arithmetic — Cody erfcx domain-1 numerator ≤0.34 ulp, normalised-Black assembly ≤1 ulp. Approximation: formal/sollya/ bounds the Cody rational against the true erf (domain 1 ≤3.3e-9, realized sub-ulp). The Gappa proofs export to gappa -Bcoq for the Coq kernel to re-check.
The Honest Boundary
What we prove — and what we still trust
A tool that tells you the limits of its own guarantees is one you can trust with the parts it does guarantee. We publish the boundary in full.
Proven
The pricing mathematics over ℝ, and the structural exposure / sign / netting logic on the real Rust. Lean-kernel-checked.
Measured
The proved relationships hold in f64 to ~1e-15 — grid testing alongside the existing MPFR-oracle reference tests.
Bounded
The kernels' rounding and approximation error, by Gappa + Sollya, with a foundational Coq-kernel export.
Still trusted
The f64 results of exp / log(libm), full end-to-end FP error composition, and SIMD/FMA reassociation. Heston's characteristic-function integral is out of scope.
Reproduce It
Re-check it yourself
The proofs aren't a marketing artifact — they are re-runnable. Every layer has a command.
cd crates/ferro-risk # 310 public ℝ-theorems and lemmas; no admitted proofs sh scripts/check-math-proofs.sh # trusted-base audit — only the three standard axioms sh formal/lean-math/check-axioms.sh # floating-point rounding bounds (Gappa) sh formal/gappa/run.sh # approximation bound vs the true erf (Sollya) nix run nixpkgs#sollya -- formal/sollya/erfcx_domain1_approx.sollya # the proved laws, measured in f64 cargo test --test formal_conformance -- --nocapture # the IV solver accuracy sweep cargo test --test iv_solver_accuracy -- --nocapture