Verification and testing

Component	Evidence	Audit
Physical vaults (EVM)	Lean 4 proofs of the settlement model, Vyper reference, Foundry invariants and Halmos checks mapped to the theorems	None
Cash-settled pools (Robinhood Chain)	Unit, lifecycle, stateful invariant and mainnet-fork tests	None
Solana pilot program	Property and differential tests	None

Physical vaults: Lean 4

The settlement core (mint, redeemPair, exercise, settle, redeemP, claim) is modelled as a state machine and proved over every reachable state, for call and put vaults. No sorry; axioms limited to propext and Quot.sound. Repo: github.com/mmchougule/split-fv.

Proved:

• No settlement transition reads a price, oracle answer or DEX reserve.
• Claims never redeem more than the vault holds.
• Exercise never releases collateral without the strike being paid.
• Rounding strands bounded dust only.
• Transitions are phase-gated; a claim can't be reused.
• The put vault satisfies the same properties with roles swapped.

Limits:

• The proofs are about the model. Foundry and Halmos conformance checks are separate evidence about the deployed Solidity.
• The deployed call vault does not include the residual-recipient terminal rule modelled for the put vault.
• Certora specs typecheck only.
• Pricing, quote signing, pools and the gasless relayer are out of scope.

The per-theorem map is conformance/THEOREM_MAP.md.

Cash-settled pools

• Unit tests for buy, sell, settle and claim on both legs.
• An end-to-end pool lifecycle test.
• A stateful invariant run asserting payouts never exceed posted collateral, on both legs.
• Fork tests against the live USDG and Chainlink feeds.
• Property tests on the pricer, including the bound that a capped leg is never valued above its width.

Not covered: formal proofs, a dispute window, and an audit. Solvency rests on construction (Up + Down = W, locked at sale) plus the invariant suite.

Audit

No third-party audit has been completed on any Split contract.