Verification
10 proven invariantssour-verification ↗Sour publishes formal proofs for every load-bearing accounting invariant — pooled-vault conservation, LP-scaled per-user cap, aggregate-budget cap, fractional CURVE LP capacity, positive-PnL conservation. Each summary below links into the machine-checkable proof in the public verification repo.
Tools: Kani (bounded model checking, CBMC backend) · Lean 4 (interactive theorem proving, no Mathlib). Proofs mirror the on-chain handlers byte-for-byte; both tools verify the as-built code, not the as-written spec.
Per-market OI cap is price-agnostic (USD-notional micros)
KANI + LEANv0.6.0 flipped Market.max_oi semantics from underlying-units to USD-notional micros so a single dollar cap (e.g. $50,000) applies uniformly to BTC at $80K mark and XRP at $1.40 mark — eliminating the per-market admin sweep operators had to run on every price move. Bound proven over u8 in Kani for the structural inequality + cross-market dollar-parity at concrete BTC/XRP mark values.
Per-user cap bounds single-position worst LP loss
KANI + LEANIf a user's notional fits under the LP-scaled per-user cap and their margin tier is below the protocol max, then their worst-case LP loss can never exceed the configured risk-budget fraction of LP NAV. Proven over u8 in Kani for the multiplicative form and over general Nat in Lean for the full cap formula.
Aggregate-cap invariant holds under update
KANIAfter each upsert, the running counter `Protocol.aggregate_max_lp_loss` stays under the aggregate cap (`total_assets × aggregate_budget_bps / max_mm_bps`) — provided the on-chain enforcement check passed. Proves the upsert hot path can't drift the counter past the cap one block at a time.
recompute_aggregate equals sum of per-market exposures
KANI + LEANThe permissionless `recompute_aggregate` instruction byte-equals the sum of per-market `worst_case_lp_loss` over the supplied markets (proven for N=4 in Kani; general N over Nat in Lean). Anyone can recompute the counter to recover from drift.
update_aggregate rejects negative-going wrap
KANIIf a cascade decrement would push the running counter below zero, `Protocol::update_aggregate` returns `Err(Underflow)` and leaves the counter unchanged — never silently wraps. Drift is observable and recoverable, not catastrophic.
CURVE LP capacity counts fractional qmax
KANISub-base-unit CURVE positions (storage `qmax_storage < FIXED_ONE`) reserve LP capacity proportional to their fractional max loss — they cannot bypass the LP cap by being 'too small to count'. Counterexample-locked regression after the v0.5.0 fix.
Positive close PnL conserves vault assets
KANIProfitable position closes can never credit the trader more than the LP vault is debited. Insufficient LP backing rejects with `ArithmeticOverflow` rather than partially-saturating the trader credit. Conservation invariant locked by both an executable counterexample test and a Kani symbolic proof.
Curve fill ratios stay in [0, 1]
KANIBoth long and short fill ratios are bounded by Q32.32 `FIXED_ONE` for any input price and bracket. Prevents pricing-side overflow paths where a fill ratio greater than 1 would mint extra qmax against the wrong side of the curve.
LP withdraw payout bounded by available assets
KANIBurning shares via `withdraw_lp` never pays out more USDC than `vault.total_assets - vault.outstanding_winner_pnl` (the available-assets envelope). Winner-pnl liabilities can't be drained by an LP withdraw.
Epsilon never exceeds configured maximum
KANIThe dynamic epsilon (gap-velocity confidence interval scaling) never exceeds the admin-configured `max_epsilon_bps` regardless of the override / dynamic / allocated-LP / total-assets inputs. Caps on top of caps; no override path bypasses the absolute ceiling.
Bounded-domain caveats and reproduce instructions live in the repo's What's NOT proven section. We are not under external audit yet — these proofs are one of two security layers, not the whole stack.