Research to Runtime: Correctness Under Adversarial Numerics

A research result and a production system are two different artifacts, and the distance between them is where correctness quietly fails. A pricing model is validated in a notebook and re-implemented in a fast language; a signal is proven on clean historical data and then run on a live feed; a strategy is backtested against one ordering of events and deployed into another. Each translation is a place where the mathematics that was checked stops being the mathematics that runs. In quantitative trading, that gap is a dominant source of model risk, and it is largely unmeasured.

This is the web reading of how MorphIQ Labs closes that gap; the download button above links the formal PDF with complete citations. The thesis is deliberately narrow and falsifiable: correctness and runtime performance are properties of the same artifact, not a trade-off between two of them — and the disciplines that keep them together are engineering contracts we can show, not adjectives we assert.

The seam

Most software-correctness effort is spent inside a single artifact: this function, given this input, returns this output. Quantitative systems fail somewhere else — at the seam between the research that established a result and the runtime that is supposed to preserve it.

The seam has a characteristic shape. A model is derived and checked in a research environment optimized for expressiveness: arbitrary precision, rich libraries, no latency budget, a fixed and friendly dataset. It is then re-expressed in a runtime environment optimized for the opposite: fixed-width arithmetic, a hard latency budget, adversarial and incomplete inputs, and event orderings no one chose. Nothing forces the second artifact to agree with the first. The tests that pass are usually the tests someone thought to write, over the inputs that occur most often — which is exactly the region where two implementations are most likely to agree and least likely to reveal a divergence.

The failures that result are not loud. They are a Greek that is correct at the money and wrong in the deep wings; an implied-volatility solver that converges to the wrong root in an admissible-but-rare region; a transform that is exact on the sample and biased on the tail; a backtest that is reproducible only because yesterday a thread won a race it will lose tomorrow. None of these throw. They produce a number, and the number is used to rank, hedge, size, or explain a decision. This is what model risk means operationally: not that the model is wrong on paper, but that the running system silently stopped being the model.

The industry's usual answer is process around the seam — model-validation groups, sign-off gates, reconciliation reports. Those are real controls, but they treat the seam as a handoff to be inspected. Our position is that the seam should not be a handoff at all.

The claim

Two things this claim is careful not to say. It does not say the artifact is "verified" in the sense that its outputs are guaranteed correct; only specific, stable primitive laws carry maintained proofs, and we are precise about which. And it does not say correctness was achieved by sacrificing speed, or speed by sacrificing correctness. The load-bearing observation is that the two do not trade against each other when the disciplines are in place from the start rather than retrofitted: a reference oracle is a test-time dependency, not a runtime one; a proof gate runs in CI, not in the hot path; determinism is a structural property, not an overhead.

The standard

We hold a layered standard. No single discipline is sufficient; each is chosen to catch a failure mode the others structurally cannot.

Reference oracles. A test that compares an implementation to itself proves only that it is self-consistent. Numerical kernels are instead checked against an independent source of truth computed at far higher precision — an arbitrary-precision oracle, or a canonical reference implementation — whose answer is trusted because it is derived differently and to more digits than the runtime path. This is the discipline that catches the deep-wing Greek and the wrong-root solver, because it evaluates agreement where the fast path is under stress. The oracle is a test dependency, never the runtime path.

Proof gates on stable laws. Where a property is a stable mathematical law — monotonicity, put-call parity, no-arbitrage bounds, the clock and interval laws of a deterministic scheduler — it is stated as a law and machine-checked in a proof assistant; where it is a required check, it gates the build. Proof gates do not replace tests; they cover the cases tests can only sample. They apply only where the law is stable enough to specify — a minority of any system, and precisely the minority whose violation is catastrophic.

Property-based testing. For behavior that is lawful but not provable in closed form, we assert the invariant and let a generator attack it across a large, randomized input space — including the pathological corners a hand-written suite omits.

Mutation testing. A passing test suite says the tests pass; it does not say the tests would notice a defect. Mutation testing deliberately injects faults and measures how many the suite kills. It is the discipline that tests the tests, and it is why a high test count is not, by itself, a correctness claim we make.

Deterministic replay. Wall-clock time, iteration order, and thread races are untested inputs in most systems. We remove them as a class: the runtime has no direct access to time or nondeterministic ordering, a constraint enforced mechanically rather than by convention, so that a backtest and a production run can be the same program over the same event tape. Determinism is what makes every other guarantee reproducible.

Bounded arithmetic. Where correctness depends on it, we do not use floating point for value-bearing quantities; kernels that must use floating point carry known error envelopes rather than hope. Rounding behavior is a specified property, not an accident of the hardware.

Benchmark gates. Performance is a contract too. Perf-sensitive paths carry benchmarks whose regressions gate the build, because an artifact that is correct but misses its latency budget has failed the same claim as one that is fast but wrong.

The evidence

A standard is only a claim until it produces artifacts. The disciplines above are documented, per engine, in a family of companion papers; the following are representative receipts, each checkable against a repository or a published paper.

Reference oracles

FerroWave anchors every numerical value in the library to a citable external authority and treats a failing reference test as a finding, not a tolerance to relax. Its methodology paper documents this catching, among others, a wavelet-normalization error latent since the project's first commit, and a Paul-wavelet admissibility-constant error inflated by three orders of magnitude — each surfaced by comparison against an analytical or canonical reference, not by a self-consistency test a buggy implementation can satisfy. FerroRisk applies the same posture with an arbitrary-precision oracle: its Greeks (all ten, for both the Black-Scholes and Black-76 models), the normalized-Black price and vega, and the underlying Gaussian numerics are validated against a 512-bit MPFR reference, gated behind a test-only feature and run in CI. Its implied-volatility solver is validated against a different independent authority — Peter Jäckel's published "Let's Be Rational" reference — because the right oracle for a solver is another trusted solver.

Proof gates

The proofs are written in Lean 4 and carry no sorry and no custom axioms; the trusted base is audited. FerroReplay carries machine-checked clock, wake, interval, and realignment laws under a blocking CI gate — though, stated precisely, these prove a specified model that mirrors the runtime surface, not the Rust code directly. FerroWave proves thirteen structural primitive-contract laws (index, length, and boundary logic) on the extracted Rust via Aeneas under a blocking gate, and separately carries $111$ theorems over $\mathbb{R}$ in Lean/mathlib — perfect reconstruction $\mathrm{IDWT}(\mathrm{DWT}(x)) = x$, Parseval energy preservation, filter orthonormality — plus Gappa floating-point bounds (Haar DWT step $\leq 1$ ulp, db2 $\leq 1.6$ ulp). FerroRisk states put-call parity, no-arbitrage price bounds, monotonicity in spot, convexity, and the Black-Scholes PDE as machine-checked Lean theorems over $\mathbb{R}$.

Mutation testing

FerroWave sets a minimum mutation-kill floor of $70\%$ and measures above $90\%$ in practice — evidence the suite detects injected faults, not merely that it is large. This is the discipline behind the claim that its more than $1{,}800$ tests have teeth, rather than the count being the claim itself.

Determinism as a contract

The deterministic-replay constraint is enforced mechanically — not by reviewer discipline — through two independent, blocking gates: a Clippy disallowed-methods lint that bans direct wall-clock and timer APIs, and a separate textual CI check that greps the source for the same tokens. Exactly one sanctioned clock module is exempt, so a backtest and a production run are the same program over the same event tape.

Release gates

FerroRisk's CI enforces formatting, Clippy warnings-as-errors, the full regression suite (which runs the MPFR oracle tests), documentation warnings-as-errors, a fuzz build check plus fuzz smoke runs, SIMD correctness under aarch64 emulation, and a required Lean model-proof gate; performance thresholds are enforced as a release gate. A release cannot silently drop a guarantee because each of these is a gate, not a guideline.

What this buys you

Rigor is not held for its own sake; it changes what you can rely on.

• Numbers you can stand behind. A risk surface whose contracts are proven or oracle-checked can be explained — parity holds, monotonicity holds, the wings are specified — rather than merely produced.
• Backtests that mean something. When production is the same program as the backtest, a result that reproduces is evidence of determinism, not of profit, and not coincidence.
• Failure where it is visible. Bounded arithmetic and stated error envelopes turn silent numerical drift into a specified, inspectable property.
• A standard that does not decay. Gates run on every commit. The correctness is a maintained contract, not a launch-day snapshot.

What we do not claim

A discussion of rigor earns trust in proportion to what it refuses to overstate. The limits are part of the standard, not a disclaimer appended to it.

• We do not call any product, platform, application, or trading strategy "formally verified." The claim is specific, stable primitive laws carrying maintained proofs — never investment outcomes, model certainty, execution quality, or risk-free trading.
• A proof boundary covers the law it specifies and nothing outside it. Where the underlying law is not stable enough to specify, we say so.
• Machine-checked does not mean blocking everywhere. The structural primitive contracts and the deterministic-clock model laws gate CI today; the deeper mathematical-law proofs over $\mathbb{R}$ are machine-checked but currently run as non-blocking proof surfaces. The Rust-extraction proofs (Aeneas) cover structural and index logic, not floating-point values, which are bounded separately. We do not claim the compiled floating-point binary is end-to-end proven.
• Rigor reduces model risk; it does not eliminate it. The residual is the part we are honest about, because a rigor practice that oversells a single claim spends more credibility than any one result can return.

Closing

The seam between research and runtime is where quantitative systems actually fail, and it is usually managed by inspecting a handoff. We do not treat it as a handoff. The same rigor that validates the research is carried into the artifact that runs — oracle-checked, proof-gated where the law is stable, mutation-tested, deterministic, and benchmarked — so that the mathematics that ships is the mathematics that was proven.

Companion papers

The formal PDF cites these engineering papers as its primary evidentiary sources: Reference-Based Numerical Validation in FerroWave; the FerroRisk pricing and implied-volatility notes (Pricing Models, Implied-Volatility Solver, Volatility Surface, Put-Call Parity and the Forward); and the FerroReplay determinism series (FerroReplay, Sequence-not-Timestamp, Crash-Tolerant Replay, Determinism as a Correctness Contract).

---

This paper describes engineering correctness practices. It is not investment advice, not an offer or solicitation, and makes no representation of trading performance or outcomes. Third-party names — including Lean, mathlib, Aeneas, Gappa, MPFR, Clippy, and "Let's Be Rational" — are marks of their respective owners, used here for identification only.