The formally verified perp DEX

What we proved with Kani

Kani is a Rust model checker built on top of CBMC and used by AWS and others to verify production Rust code. It is bounded model checking on the actual program — no separate model in a different language, no hand-translation of the code into a math toy. You write properties as ordinary Rust assertions, declare which inputs are non-deterministic, and Kani exhaustively explores every input within the bound. If a property holds, it holds for every input of that size. Not "it holds on the inputs we happened to think of", which is what unit tests check. Every input.

Sour ships eighteen Kani proofs over the on-chain settlement code. They cover the parts where a single off-by-one or a wrong sign on a signed integer would silently corrupt PnL: per-trade settlement preserves total value (winners gain exactly what losers lose, no USDC is created or destroyed by the matching engine), aggregate Open Interest never exceeds the LP-NAV-scaled budget after any partial fill, no-bad-debt invariants hold under price-move scenarios where positions cross the liquidation boundary inside a single batch, and the curve-bracket and clear-batch handlers preserve the pooled-vault sum invariant (vault USDC equals total assets plus the sum of trader collateral, byte-exactly).

Each of those proofs is more than a unit test, and more than a fuzzer. A fuzzer is sampling. A bounded model checker enumerates. Within the bound — number of traders, number of fills, magnitude of inputs — the property is true for every assignment of every variable, including the assignments that no human would think to write down. That is what "verified" means in this context.

What we proved with Lean

Lean is a theorem prover. It is a different beast from Kani: where Kani searches a bounded space of concrete inputs, Lean reasons about all inputs symbolically, including the unbounded ones. The trade-off is that Lean proofs do not run on the real Rust code; they run on a specification of the algorithm written inside Lean itself. They are stronger statements over a smaller surface.

Sour ships one Lean specification: the Option H aggregate-budget enforcement, modeled and proven for general N. The aggregate-budget rule says that the sum of every trader’s open notional, weighted by the per-market initial-margin requirement, never exceeds the LP NAV scaled by the configured risk-budget bps. The Lean proof shows that, in the model, this property is preserved by every state transition the spec admits — for any number of traders, any sequence of opens and closes, any combination of markets. This is a statement that bounded model checking cannot make. It only holds in the model, but in the model, it holds without an upper bound.

The Lean spec and the Kani proofs are designed to overlap. Lean tells us the math is sound. Kani tells us the Rust we actually ship implements that math up to the bound it explores. Property tests close the rest of the gap.

What property tests catch that the above don’t

Sour ships fifteen generative property tests using proptest. They run in CI on every commit. Each test fixes a property — a post-condition over the program state — and lets proptest generate thousands of randomized inputs across realistic distributions, shrinking failures to minimal counterexamples when one is found.

Property tests are weaker than Kani per-input (they sample, they do not enumerate) but they cover surface area Kani does not: the integration seams between instruction handlers, the way deserialization interacts with the math, sequences of operations that are too long for bounded model checking to exhaust. They are how we catch regressions where the math handlers in isolation are correct but the way they are composed inside a real ix flow is not. Together, the three layers — proptest for integration, Kani for bounded exhaustive, Lean for unbounded symbolic — give a much stronger correctness story than any single one of them alone.

What this does not replace

Formal verification is not a substitute for a security audit. It is a stronger correctness signal over a strictly smaller scope. Be precise about the scope, because anyone who tells you otherwise is selling something.

• ACCOUNT VALIDATION IS NOT IN SCOPE
  CPI safety checks, signer verification, owner checks on incoming accounts, and the standard Solana-specific footguns are reviewed by hand. They are not part of the Kani or Lean proofs. A traditional audit would specifically examine these.
• DESERIALIZATION EDGE CASES ARE NOT IN SCOPE
  The verified math operates on already-deserialized account state. The bytes-to-state boundary — packed-struct alignment, discriminator collisions, account-size invariants — is hand-reviewed and unit-tested but is not in the formal model.
• ORACLE BINDING IS HAND-REVIEWED
  The Pyth Pull oracle adapter is reviewed manually for staleness, confidence-interval handling, and price-units conversion. The conversion math is property-tested. The end-to-end binding is not formally proven.
• UPGRADE AUTHORITY AND ADMIN FLOWS ARE OUT OF SCOPE
  The verifier focuses on the trading hot path. Pause flags, fee parameter updates, and upgrade-authority handling are deliberately outside the formal model. A traditional audit would specifically examine these surfaces.
• NO THIRD-PARTY SECURITY AUDIT YET
  Sour has not been audited by a third-party security firm. We will commission an audit; we have not yet. Trade accordingly. The verification repository is public so you can read exactly what is and is not proven, instead of taking our word for it.

Why this still matters

For the surface area that is covered — settlement preservation, aggregate-margin enforcement, no-bad-debt under price moves, pooled-vault sum invariants — formal verification is a strictly stronger correctness guarantee than any audit. Audits are humans reading code. Humans miss things. They miss boundary conditions, they miss the seventh case in a switch, they miss the path where a partial fill leaves a one-lamport residue. A machine-checked proof does not miss those, because the machine enumerates them.

The honest framing is this: verification gives you exhaustive guarantees on a small, important kernel. An audit gives you human-pattern-matched guarantees over a large surface. Most DeFi protocols ship with the audit and call that enough. Sour ships with verification today and is openly missing the audit. We think the math kernel is the right place to put the strongest guarantee, because that is where billions of dollars can vanish from a single off-by-one. We also think you deserve to know what is and is not covered before you trust the protocol with collateral.

The program ID on Solana mainnet is souryQgnM1xiNuGcmVYLPGT3MKqnGN8QTqP8zk8eape. The verifier sources are at github.com/GageBachik/sour-verification. Read both before you take a position.

At a glance

PROGRAM ID

souryQgnM1xiNuGcmVYLPGT3MKqnGN8QTqP8zk8eape

KANI PROOFS

18 model-checked over Rust settlement code

LEAN MODELS

1 general-N aggregate-budget specification

PROPERTY TESTS

15 proptest harnesses in CI

VERIFICATION REPO

github.com/GageBachik/sour-verification

PROTOCOL REPO

github.com/GageBachik/sour

THIRD-PARTY AUDIT

Not yet commissioned — be aware

NETWORK

Solana mainnet-beta

COLLATERAL

USDC

MAX LEVERAGE

50× isolated