Audits & formal verification

No third-party audit yet

A traditional smart-contract audit pays a security firm to examine the program's code surface — account validation, signer checks, CPI safety, deserialization edge cases, upgrade-authority handling — and flag patterns that are hard to catch with formal tools. Audits are scope-bounded and human-rate-limited, but they are the canonical correctness signal in DeFi.

Sour has not had this work done by a third party. We will publish the firm and the report URL on this page when it lands. Until then, the open-source surface, the formal verification record, and the responsible-disclosure channel are the substitutes — and we don't pretend they cover the same ground.

What we have proved with formal verification

Formal verification is a stronger correctness statement than testing — for the parts of the program it covers, the math is exhaustive within bounded sizes. Sour's verification work is open-source and re-runnable: github.com/GageBachik/sour-verification.

• 18 Kani model-checked proofs
  Kani is a Rust model checker that runs bounded model checking on actual Rust code. Our proofs cover settlement preservation, partial-fill correctness, no-bad-debt invariants under price-move scenarios, and the per-user OI cap. Within bounded input sizes the property holds for every input — not just the ones a unit test would have hit.
• Lean specification of the aggregate budget
  Option H general-N aggregate model, machine-checked clean. End-to-end correctness statement for the cross-trader budget enforcement.
• 15 generative property tests
  Proptest harnesses generate random inputs across realistic distributions and check post-conditions on every CI run. Catches integration regressions across instruction handlers that the math proofs don't scope.

What formal verification does not cover

We are explicit about scope. The proofs above guarantee math correctness inside their bounds. They are not equivalents for an audit.

• Account validation logic — signer checks, owner checks, PDA derivation correctness — are not in the math proofs.
• Deserialization edge cases (e.g. crafted instruction data that lies about its layout) are out of scope.
• Oracle binding correctness was hand-reviewed but is not formally proven end-to-end.
• CPI safety, upgrade-authority handling, and Solana-specific runtime behavior require human audit review.

Pointers

Program source

github.com/GageBachik/sour

Verification repo

github.com/GageBachik/sour-verification

In-app proven invariants

app.sour.finance/verification

Mainnet program ID

souryQgnM1xiNuGcmVYLPGT3MKqnGN8QTqP8zk8eape

Responsible disclosure

security@sour.finance

Bug bounty

Informal — see /security

Third-party audit

Not yet

How to use this information

If you are a trader: the formal verification work covers the math your collateral depends on, but a third-party audit is still missing. Size positions accordingly.

If you are a security researcher: the program is open source, mainnet, and live. Coordinated disclosure goes to security@sour.finance. We respond.

If you are an LP: the per-user OI cap and the aggregate budget are both proven. The risk you carry is the trader-PnL flow into and out of the vault, which is exactly the LP's job — but you are not absorbing math errors as well, which is the part the verification work eliminates.