Formal Verification of a Solana Trading Program with Certora

An audit will tell you a reviewer read your code and didn't spot a way to drain it. Formal verification tells you that no input, in any ordering, can violate a property you wrote down. Those are different guarantees, and the gap between them is exactly where settlement programs lose money. A human reviewer working through a Solana program at 200 lines an hour will trace the happy path, poke at the obvious overflow, and move on. The bug that costs you is the one that only appears when a settle instruction runs against an account whose filled_qty was mutated by a partial fill three transactions earlier, with a lookup table swapping in an attacker-controlled vault. Symbolic execution finds that. Eyes usually don't.

This is about proving no-fund-loss on a real settlement program, the tooling reality on Solana specifically, and where the approach earns its keep versus where it wastes a week.

What a settlement program actually needs to guarantee

Take a program that matches maker and taker orders and moves tokens between two vaults on settle. The properties that matter aren't "the code compiles." They're conservation laws:

• Token conservation. The sum of all vault balances plus in-flight amounts is invariant across any instruction. Tokens are never minted or burned by the settlement logic itself.
• Monotonic fills. filled_qty only ever increases, and never past order_qty.
• Authority isolation. A settlement can only debit a vault whose PDA derives from the order's own seeds.

That third one is where Solana bites differently than EVM. There's no msg.sender; authority is a function of which account you passed and how its address was derived. A verification spec that doesn't model PDA derivation is verifying a fiction. If you've done real work on multi-vault programs you already know the seed layout is load-bearing, and it's worth reviewing how PDA seed design shapes multi-vault trading programs before you write a single invariant, because the spec has to mirror those seeds exactly.

The Solana tooling caveat, up front

Certora Prover is built for EVM bytecode and CVL (Certora Verification Language) targets Solidity. It does not run natively on SBF, the eBPF-derived bytecode Solana programs compile to. Anyone who tells you they "ran Certora on your Anchor program" without qualification is either using Certora's newer Rust/SBF support (which exists but is younger and covers a narrower surface) or is quietly reimplementing the settlement logic in a verifiable model and proving that. Be honest about which one you're doing.

In practice three routes are real today:

1. Certora's Rust prover for SBF, still maturing, best for isolated pure functions like your matching math.
2. Kani, the Rust model checker built on CBMC, which does bounded symbolic execution over your actual Rust. This is the workhorse for most Anchor codebases.
3. A hand-written model of the state machine that you verify with an SMT solver directly.

For a settlement program I reach for Kani first because it runs against real code, and I fall back to a model when the account-loading machinery makes the real code too noisy to reason about.

Writing the invariant

Here's the core matching function extracted so it can be checked in isolation — no account deserialization, just the arithmetic that must never lose value.

pub fn apply_fill(maker: &mut Order, taker: &mut Order, px: u64) -> Result<u64, FillError> {
    let avail_maker = maker.qty.checked_sub(maker.filled).ok_or(FillError::Underflow)?;
    let avail_taker = taker.qty.checked_sub(taker.filled).ok_or(FillError::Underflow)?;
    let fill = avail_maker.min(avail_taker);
    maker.filled = maker.filled.checked_add(fill).ok_or(FillError::Overflow)?;
    taker.filled = taker.filled.checked_add(fill).ok_or(FillError::Overflow)?;
    Ok(fill)
}

The Kani harness asserts the conservation property over every reachable input, not a fixed test case:

#[kani::proof]
fn fill_conserves_and_bounds() {
    let mut maker: Order = kani::any();
    let mut taker: Order = kani::any();
    kani::assume(maker.filled <= maker.qty);
    kani::assume(taker.filled <= taker.qty);

    let before = maker.filled + taker.filled; // widened to u128 in practice
    if let Ok(fill) = apply_fill(&mut maker, &mut taker, kani::any()) {
        assert!(maker.filled <= maker.qty);          // never over-fills
        assert!(taker.filled <= taker.qty);
        assert_eq!(maker.filled + taker.filled, before + 2 * fill);
        assert!(fill > 0 || maker.qty == maker.filled || taker.qty == taker.filled);
    }
}

kani::any() is the whole point. It's not a random value; it's a symbolic one, and the solver searches for any assignment that breaks an assertion. Run cargo kani --harness fill_conserves_and_bounds and either it proves the property across the full u64 space or it hands you a concrete counterexample — the exact qty/filled/px triple that breaks it. That counterexample is the deliverable. It's a failing test case you didn't have to imagine.

The first time I ran a harness like this on a real program, the counterexample was a px of zero producing a valid fill with a downstream quote amount of zero — a settlement that moved base tokens for nothing. No fuzzer in the suite had hit it because the price feed never legitimately produced zero, but nothing in the program forbade it.

The gotchas that eat your week

State explosion is real. Kani unwinds loops. If your matching engine walks an orderbook, you must bound the unwind (#[kani::unwind(8)]) or it runs forever. This forces a design conversation: prove the single-fill step exhaustively, then prove the loop separately with an inductive argument. Programs using zero-copy Anchor accounts for on-chain orderbook state are actually easier here, because the flat [Order; N] layout gives you a fixed, bounded array instead of a Vec the solver can't size.

Account loading is not verifiable Rust. Anchor's #[account] deserialization, Context, and the runtime's account model don't exist inside Kani. You verify the logic, and you cover the account-authority boundary with something else. Which means the spec has an assumption baked in: "the right accounts were passed." That assumption is a lie precisely when a lookup table reorders or substitutes accounts, which is the failure mode worth understanding in address lookup tables and multi-leg arb transactions. Formal verification of the math does not cover that seam. A review still has to.

Proving assume isn't hiding the bug. Every kani::assume narrows the input space. Assume too much and you've proven a property about inputs that never occur, which is worthless. The discipline is to keep assumptions to genuine on-chain invariants (an account can't have filled > qty because a prior instruction enforced it) and never to paper over a case you're too lazy to handle.

Where this fits against an audit

Formal verification and audit aren't substitutes. Verification proves the properties you thought to write; it says nothing about the property you forgot. An audit catches the missing property — the reviewer who asks "what stops a self-trade?" when your spec never mentioned self-trades. The strongest settlement work pairs both: a verification pass that makes conservation and bounds machine-checked, and a focused code review and audit that hunts for the invariants you didn't write down and the account-authority seams the solver can't see.

If you're standing up a new settlement or matching program, the cheapest time to make properties provable is while the smart-contract development is still in flight — bolting a verifiable model onto a finished program costs three times as much as designing the state to be checkable from day one.

If you want a settlement program whose no-fund-loss properties are machine-proven rather than merely reviewed, that's exactly the kind of work our smart-contract development team builds to spec.