Research & Verified

Split is an oracle-free, physically settled options primitive: settlement reads no ETH/USD price, so settlement safety is an accounting property, not a price property. That core is machine-checked in Lean 4, and the pricing and LP economics are backed by simulation against real market data.

Formal verification

The settlement core (mint, redeemPair, exercise, settle, redeemP, claim) is modeled as a state machine, and its safety theorems are proved in Lean 4 over every reachable state, for both the call and put vaults. The proofs are axiom-clean (propext, Quot.sound) with no sorry.

• Repo: github.com/mmchougule/split-fv

What the theorems establish

• Oracle independence (structural). No settlement transition reads an ETH/USD price, oracle answer, or DEX reserve, so the usual price-manipulation drain vector is removed by construction, not by assumption.
• Backing. Claims can never redeem more than the vault holds.
• Exercise pays. Exercise can never take collateral without paying the strike.
• Bounded rounding. Rounding can only strand bounded dust, never drain the pool.
• Phase safety and no double-claim. Transitions are phase-gated, and a claim can't be reused.
• Put symmetry. The put vault proves all of the above with the roles swapped.

How the layers fit

• Lean is the source of truth.
• A Vyper reference implementation compiles and passes its property tests.
• A Solidity conformance suite (Foundry stateful invariants and Halmos symbolic checks) maps one-to-one to the theorem names, checking the shipped contracts behave the same.

Scope and honesty

• The proofs cover the settlement core only. Pricing and quote signing, the keeper, the LP pool, and the gasless facilitator are out of scope, and that is where economic risk concentrates.
• Lean theorems prove properties of the model. Conformance checks are separate evidence about the deployed Solidity; not every deployed bytecode path is itself proven. One known model-vs-code gap: the deployed call vault does not yet implement the residual-recipient terminal rule that the put vault does.
• Certora specs typecheck only (no cloud verdict yet).
• This is a machine-checked settlement-core safety argument, not a third-party audit.

The per-theorem scoreboard (Lean → Vyper → Foundry → Halmos → Certora) lives in conformance/THEOREM_MAP.md.

Pricing

Premiums use the Black-Scholes model with an implied-volatility input, plus a jump component that accounts for sudden price moves. The same pricing math powers quotes, marks, and the greeks shown on each position.

LP economics

Writers (LPs) earn the option premiums along with trading fees and the spread generated by volume. The LP value proposition (premium income against the drawdowns of writing options through fast moves) is modeled with Monte Carlo over real ETH paths and cross-referenced against other liquidity vaults. Findings and the simulation code live in the repo under docs/research/.

   premium income  ▁▂▃▄▅▆▇   steady, every round
   gap drawdown          ▼     rare, large, on fast moves
   net to LP        ▁▂▃▄▅ ▼ ▃▄  premiums + fees + spread, minus gap events

Greeks

Each position exposes delta, gamma, theta, and vega from the signed quote, so risk is visible rather than implied. The exit logic uses delta (which encodes time to expiry) to cut positions on their actual state rather than on an arbitrary clock.