DEV Community

ohmygod
ohmygod

Posted on

Beyond Fuzzing: How the Certora Solana Prover Catches Bugs at the Bytecode Level That Fuzzers Miss

#solana #security #defi #web3

Your fuzzer ran for 72 hours. Zero crashes. Your unit tests hit 95% coverage. You shipped with confidence.

Then someone drained $4 million because the Rust compiler optimized away a critical bounds check that existed in your source code but vanished in the compiled SBF bytecode.

Welcome to the verification gap — the space between what your source code says and what the Solana runtime actually executes. Fuzzers test what you wrote. Formal verification tools like the Certora Solana Prover (SCP) prove properties about what the machine runs.

The Problem: Your Source Code Isn't What Runs On-Chain

Every Solana program goes through a compilation pipeline:

Rust Source Code
    ↓ rustc + LLVM
Intermediate Representation (IR)
    ↓ LLVM Backend
Solana Binary Format (SBF)  ← This is what actually executes
    ↓
Solana Runtime (rbpf VM)
Enter fullscreen mode Exit fullscreen mode

At each stage, transformations occur. Dead code elimination, constant folding, loop unrolling, function inlining — the compiler makes dozens of optimization decisions that can subtly change program behavior.

Most audit tools operate at the source level. They analyze your Rust code, check for known vulnerability patterns, and report findings. But they're blind to bugs introduced by the compiler itself.

Real-World Example: The Phantom Overflow

Consider this simplified Solana program logic:

pub fn process_transfer(
    amount: u64,
    fee_bps: u16,
    recipient_balance: u64,
) -> Result<u64, ProgramError> {
    let fee = amount
        .checked_mul(fee_bps as u64)
        .ok_or(ProgramError::ArithmeticOverflow)?
        .checked_div(10_000)
        .ok_or(ProgramError::ArithmeticOverflow)?;

    let net_amount = amount
        .checked_sub(fee)
        .ok_or(ProgramError::ArithmeticOverflow)?;

    let new_balance = recipient_balance
        .checked_add(net_amount)
        .ok_or(ProgramError::ArithmeticOverflow)?;

    Ok(new_balance)
}
Enter fullscreen mode Exit fullscreen mode

Source-level analysis says this is safe: every arithmetic operation uses checked math. But what if the compiler determines that fee_bps is always loaded from a constant account and optimizes the multiplication to a shift operation that doesn't preserve the overflow check?

This isn't hypothetical. Compiler optimizations have caused verified-safe Rust code to behave unsafely in compiled form.

Enter the Certora Solana Prover

The Certora Solana Prover (SCP) takes a fundamentally different approach: it analyzes the compiled SBF bytecode directly.

How SCP Works

Instead of pattern-matching on source code, SCP:

  1. Disassembles the SBF binary into an intermediate representation
  2. Builds a mathematical model of all possible execution paths
  3. Checks your specification (written in CVL) against every possible input
  4. Returns either a proof that the property holds, or a concrete counterexample showing how it can be violated

What SCP Catches That Fuzzers Miss

1. Compiler-Introduced Vulnerabilities — SCP analyzes the actual bytecode. If the compiler introduces a subtle bug, SCP will find it.

2. Cross-Program Invocation (CPI) Issues — SCP can model CPI effects and verify that no sequence of cross-program calls violates an invariant.

3. Account Deserialization Edge Cases — SCP exhaustively verifies that no malformed account data causes incorrect behavior.

4. Integer Precision Loss — Fuzzers test random inputs. SCP tests all inputs.

Head-to-Head: SCP vs Traditional Audit Tools

Use fuzzers when: You want to find crashes quickly and test complex state transitions.

Use static analysis when: You want fast CI/CD integration and pattern-based checks.

Use SCP when: You're building critical DeFi infrastructure and need mathematical guarantees.

The optimal approach: all three. They're complementary, not competing.

Development Lifecycle:
Write Code → Static Analysis (CI gate) → Fuzz 72+ hours → Formal Verify (SCP) → Manual Audit
Enter fullscreen mode Exit fullscreen mode

Practical Setup: Getting Started with SCP

Step 1: Install the Certora CLI 

pip install certora-cli-beta
Enter fullscreen mode Exit fullscreen mode

Step 2: Compile to SBF 

cargo build-sbf
Enter fullscreen mode Exit fullscreen mode

Step 3: Write CVL Specification 

methods {
    function transfer(address, address, uint64) external;
    function get_balance(address) external returns uint64 envfree;
    function get_total_supply() external returns uint64 envfree;
}

invariant supply_conservation()
    get_total_supply() == INITIAL_SUPPLY

rule transfer_within_balance {
    address sender; address receiver; uint64 amount;
    uint64 sender_balance = get_balance(sender);
    require amount > sender_balance;
    transfer@withrevert(sender, receiver, amount);
    assert lastReverted;
}
Enter fullscreen mode Exit fullscreen mode

Step 4: Run the Prover 

certoraRun target/deploy/your_program.so \
    --spec spec/token_safety.cvl \
    --solana \
    --msg "Token safety verification"
Enter fullscreen mode Exit fullscreen mode

Integrating AI Audit Tools: The Force Multiplier

SCP provides mathematical certainty. AI audit tools like Nethermind's AuditAgent and Sherlock AI provide coverage breadth. Together, they create defense-in-depth:

  • AI for spec generation: Translate natural language requirements into CVL starting points
  • AI for invariant discovery: Let AI analyze your codebase and suggest invariants you hadn't considered
  • SCP for proof: Take AI-suggested invariants and mathematically prove them

Case Study: Verifying a Solana Lending Protocol

Critical properties to verify:

  1. Solvency: Protocol always has enough tokens to cover withdrawals
  2. Liquidation safety: Undercollateralized positions can always be liquidated
  3. Interest accrual: Interest never causes balance underflow
  4. Oracle freshness: Stale oracle data blocks new borrows 
Certora Solana Prover Results:
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
✓ protocol_solvent            [VERIFIED]     42.3s
✗ liquidation_always_possible [VIOLATED]     18.7s
  Counterexample: dust position (1 lamport borrow) 
  can't be liquidated — reward < minimum threshold
✓ interest_accrual_safe       [VERIFIED]     31.1s
✓ stale_oracle_blocks_borrows [VERIFIED]     12.8s
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
3/4 rules verified. 1 violation found.
Enter fullscreen mode Exit fullscreen mode

The SCP found a real bug in 18 seconds that a fuzzer might take days to discover: dust positions create unkillable zombie debt.

What's Coming in 2026

  • Multi-program verification: Verify properties across interacting Solana programs
  • Token-2022 extension modeling: Verify transfer hook logic preserves token conservation
  • Firedancer compatibility checking: Ensure programs behave identically on both runtimes
  • AI-assisted spec writing: Reduce the barrier from PhD-level to senior-developer-level

Action Items

  1. Add SCP to your audit pipeline — catches bugs that manual review can't
  2. Start with conservation invariants — "tokens in = tokens out" is highest-value
  3. Use AI tools to bootstrap specs — don't write CVL from scratch
  4. Run fuzzers AND SCP — they find different bug classes
  5. Verify bytecode, not source — the compilation gap is real
  6. Budget 2-3 days for spec work per major program component

Your Rust code is a suggestion. The SBF bytecode is the truth. Verify accordingly.

Building on Solana? The Certora Solana Prover is available in beta. Start with one critical invariant and expand from there.

Top comments (0)