What a Rust Options Pricing Engine Has to Prove

A Rust options pricing engine usually gets judged by surface area first: how many models, how many Greeks, how fast the implied-volatility solver runs. That is necessary, but it is not enough. The harder question is whether the engine preserves the mathematical contracts a downstream system is going to rely on.

For options analytics, those contracts are not decorative. Put-call parity, monotonicity in volatility, no-arbitrage bounds, convexity, and solver existence are the difference between a risk surface that can be explained and a number generator that happens to pass common test cases.

The contracts that matter

The stable parts of a pricing engine should be stated as laws. Some examples:

• A call price should be nondecreasing in spot and volatility.
• Put-call parity should hold under the model assumptions.
• Implied volatility should be unique inside the model's admissible region.
• Boundary behavior should be explicit near zero time, zero volatility, deep wings, and rates.
• Floating-point kernels should carry known error envelopes.

Those are not product claims. They are engineering contracts. If another component uses Greeks to rank candidates, hedge exposure, or explain a risk decision, the pricing layer has to make clear which contracts are proven, which are measured, and which still depend on model assumptions.

Why proof gates belong beside tests

Reference tests catch regressions against known implementations. Property tests search a larger state space. Formal proofs do something different: they reduce a claim to an explicit mathematical statement and machine-check the derivation.

That is why MorphIQ Labs treats formal methods as a gate, not a slogan. In FerroRisk, the real-valued pricing identities and primitive laws live in the proof layer; the floating-point kernels are bounded separately; the production Rust implementation is benchmarked and tested against reference oracles. Each layer does the part it can actually defend.

Performance is still part of the contract

Proof-gated math is not an excuse to ship slow code. In a production analytics pipeline, latency determines whether a model can be used interactively, reranked across a chain, or replayed through a journal. The hot path still has to be measured in nanoseconds, and performance regressions need the same discipline as correctness regressions.

The useful framing is simple: correctness defines what the number means; performance defines where it can be used.

See the public FerroRisk verification surface: ferrorisk.morphiqlabs.com/verification.