Research

What is proven, what is tested, and what the design changes.

• Why nobody gets liquidated: full collateral instead of margin.
• What this design changes: the usual failure modes of on-chain options, one by one.
• Verification and testing: Lean proofs for the physical vaults, test suites for the cash-settled pools, no audit yet.

Formal verification

The physical settlement core (mint, redeemPair, exercise, settle, redeemP, claim) is modelled as a state machine in Lean 4 and proved safe over every reachable state, for the call and the put vault. Repo: github.com/mmchougule/split-fv.

The proofs do not cover the cash-settled pools that run current trading.

Pricing

Black-Scholes with a jump component, priced as a call spread on capped bands. See Pricing.

Writer economics

A Monte Carlo of a fully collateralized covered-call writer on real ETH paths. It is a scenario model, not observed returns. See Writer economics.