The integral framing here is the key bit - loss(price) integrates to a finite bound, so you lock up exactly that much collateral once and never need liquidations. The second half of that the collateral actually covers the bound, on-chain, across every reachable state is the part I went and made machine-checked. I built the physically-settled version (1 ETH → P + N; exercise = N pays the fixed strike in and takes collateral out, no price read at settlement), it’s live on Base mainnet now, capped beta, but real on-chain settlement: https://split.markets.
The question I’d flagged earlier was whether “exercise replaces the oracle” actually holds at the protocol level, or whether an oracle quietly sneaks back into settlement. I made that falsifiable. The settlement core is proved over all reachable states, for both the call and put vaults — two properties worth surfacing:
-
No oracle at settlement, as a theorem. Non-interference: model an arbitrary external world
w(a price, a Chainlink answer, DEX reserves), lift the settlement transition over it, and prove∀ w₁ w₂ s st, applyIn w₁ s st = applyIn w₂ s st. It’s definitional precisely because the transition’s type admits no price input — there is nothing to manipulate. -
Solvency = the finite bound, formalized. Vault holdings always cover every claim, value is conserved, rounding is always toward the vault — across every reachable state. That’s the on-chain side of “set collateral equal to the finite integral.”
What we checked at six layers, each mapped one-to-one to the same theorem names.
-
Lean 4 - the proofs themselves;
#print axiomsclean (propext/Quot.sound, nosorry). -
Verity - an independent second mechanization that *also lowers to EVM bytecode*, zero
sorry/ zero custom axioms. -
Vyper - a readable reference implementation with property tests.
-
Foundry - stateful invariants run directly against the shipped Solidity.
-
Halmos - symbolic execution over every settlement selector, including an oracle “canary” that is never touched.
-
Static bytecode pass - every external call in the contract’s runtime code resolves only to the vault’s own immutable token addresses. there is no hardcoded, calldata-derived target, or delegatecall escape.
Scope: the proofs cover settlement. Pricing is an off-chain signed quote checked on-chain at trade time. Open-sourcing the formal verification repo next.
The part I’d most value getting attacked: is non-interference over an arbitrary external world the strongest standard way to formalize “this settlement cannot depend on any external price”? It’s live, try it and tell me where it breaks.