Certora CVL tutorial: a practitioner's guide to writing specs

If you've been auditing DeFi protocols for any length of time, you've probably run into Certora. It's the most widely used formal verification platform in the EVM space, and for good reason. When you need mathematical proof that a property holds across every possible execution path, Certora delivers.

But writing CVL specs isn't easy. The docs are dense and the error messages can be cryptic. There's a real learning curve between "I understand what formal verification does" and "I can write a useful spec for a production protocol." This guide bridges that gap.

What is CVL?

CVL stands for Certora Verification Language. It's a domain-specific language for writing formal specifications of smart contracts. You write rules and invariants that describe what your contract should do, and Certora's Prover checks whether the actual implementation satisfies those specs.

Think of it as writing executable documentation that the machine can verify. If your spec says "solvency always holds," the Prover either confirms it or gives you a concrete counterexample showing how solvency breaks.

How it differs from fuzzing

Fuzzing tests many random inputs. Certora tests all inputs symbolically. That's the core difference.

But there's more to it:

• Fuzzing works with Solidity test files. Certora uses a separate spec language (CVL).
• Fuzzing is best for stateful, multi-transaction properties. Certora excels at single-transaction and two-transaction properties.
• Fuzzing is fast to set up. Certora has a steeper learning curve but gives stronger guarantees.

For a deeper comparison, check our fuzzing vs formal verification guide. They're complementary, not competing.

Setup and installation

You'll need:

1. Python 3.8+
2. Java 11+ (for the solver backend)
3. A Certora API key (get one from certora.com)

Install the Certora CLI:

pip install certora-cli

Set your API key:

export CERTORAKEY=<your-api-key>

Verify it works:

certoraRun --version

Project structure

A typical Certora setup alongside a Foundry project looks like this:

project/
  src/
    Token.sol
    Vault.sol
  certora/
    specs/
      Token.spec
      Vault.spec
    helpers/
      TokenHelper.sol
    conf/
      Token.conf
      Vault.conf

The specs/ directory holds your CVL files. helpers/ has Solidity wrapper contracts that expose internal functions or simplify verification. conf/ has JSON configuration files for certoraRun.

CVL basics: rules

A rule is the basic unit of a CVL spec. It describes what should happen when a function is called:

rule transferUpdatesBalances(address sender, address receiver, uint256 amount) {
    // Preconditions
    require sender != receiver;
    require sender != 0;

    // Capture state before
    uint256 senderBalBefore = balanceOf(sender);
    uint256 receiverBalBefore = balanceOf(receiver);

    // Execute function
    env e;
    require e.msg.sender == sender;
    transfer(e, receiver, amount);

    // Postconditions
    assert balanceOf(sender) == senderBalBefore - amount,
        "Sender balance should decrease by amount";
    assert balanceOf(receiver) == receiverBalBefore + amount,
        "Receiver balance should increase by amount";
}

Key concepts:

• env e: Represents the transaction environment (msg.sender, msg.value, etc.)
• require: Preconditions. These constrain the input space. They don't weaken the verification; they define which scenarios you're testing.
• assert: The property that must hold. If the Prover finds any execution where this is false (given the preconditions), it produces a counterexample.

Invariants

An invariant is a property that should hold at all times — before and after every function call:

invariant totalSupplyIsSumOfBalances()
    totalSupply() == sumOfBalances
    {
        preserved with (env e) {
            require e.msg.sender != 0;
        }
    }

The preserved block adds constraints that should hold whenever a function is called. The Prover checks that the invariant holds in the initial state and that every function preserves it.

Invariants are incredibly powerful for DeFi. Some examples:

• Total supply equals sum of all balances
• Total deposited collateral >= total borrows (for a lending protocol)
• LP share price is monotonically non-decreasing (for a vault)

Ghosts and hooks

Ghosts are auxiliary variables that don't exist in the contract but help you write specs:

ghost uint256 sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance) {
    sumOfBalances = sumOfBalances + newBalance - oldBalance;
}

The hook triggers whenever balanceOf gets written to storage. It updates our ghost variable to track the sum. This pattern is everywhere in DeFi verification. You can't directly iterate over a mapping in Solidity, so ghosts let you track aggregate properties.

A complete example: ERC-20 spec

Let's put it all together. Here's a real CVL spec for a basic ERC-20 token.

methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function allowance(address, address) external returns (uint256) envfree;
    function transfer(address, uint256) external returns (bool);
    function transferFrom(address, address, uint256) external returns (bool);
    function approve(address, uint256) external returns (bool);
    function mint(address, uint256) external;
    function burn(address, uint256) external;
}

// Ghost to track sum of all balances
ghost uint256 sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address user] uint256 newBal (uint256 oldBal) {
    sumOfBalances = sumOfBalances + newBal - oldBal;
}

// === INVARIANTS ===

invariant totalSupplyMatchesSum()
    totalSupply() == sumOfBalances;

invariant zeroAddressHasNoBalance()
    balanceOf(0) == 0;

// === RULES ===

// Transfer correctness
rule transferCorrectness(address to, uint256 amount) {
    env e;
    require e.msg.sender != to;
    require e.msg.sender != 0;
    require to != 0;

    uint256 fromBefore = balanceOf(e.msg.sender);
    uint256 toBefore = balanceOf(to);

    transfer(e, to, amount);

    assert balanceOf(e.msg.sender) == fromBefore - amount;
    assert balanceOf(to) == toBefore + amount;
}

// Transfer reverts on insufficient balance
rule transferRevertsOnInsufficientBalance(address to, uint256 amount) {
    env e;
    require balanceOf(e.msg.sender) < amount;

    transfer@withrevert(e, to, amount);

    assert lastReverted, "Transfer should revert when balance is insufficient";
}

// Approve sets allowance correctly
rule approveCorrectness(address spender, uint256 amount) {
    env e;

    approve(e, spender, amount);

    assert allowance(e.msg.sender, spender) == amount;
}

// TransferFrom respects allowance
rule transferFromRespectsAllowance(address from, address to, uint256 amount) {
    env e;
    require from != to;

    uint256 allowanceBefore = allowance(from, e.msg.sender);
    uint256 fromBefore = balanceOf(from);
    uint256 toBefore = balanceOf(to);

    transferFrom(e, from, to, amount);

    assert balanceOf(from) == fromBefore - amount;
    assert balanceOf(to) == toBefore + amount;
    // Allowance should decrease (unless it was max uint256)
    assert allowance(from, e.msg.sender) == allowanceBefore - amount
        || allowanceBefore == max_uint256;
}

// No function changes other users' balances
rule noUnexpectedBalanceChanges(method f, address user) {
    env e;
    calldataarg args;
    require user != e.msg.sender;

    uint256 balBefore = balanceOf(user);

    f(e, args);

    uint256 balAfter = balanceOf(user);

    assert balAfter >= balBefore
        || f.selector == sig:transferFrom(address, address, uint256).selector
        || f.selector == sig:burn(address, uint256).selector,
        "Only transferFrom and burn can decrease another user's balance";
}

// Mint increases totalSupply
rule mintIncreasesTotalSupply(address to, uint256 amount) {
    env e;
    require to != 0;

    uint256 supplyBefore = totalSupply();

    mint(e, to, amount);

    assert totalSupply() == supplyBefore + amount;
}

The methods block

The methods block at the top declares the contract interface. The envfree keyword means a function doesn't depend on the environment (msg.sender, etc.), meaning it's a view function. This helps the Prover analyze things faster.

Configuration

Create certora/conf/Token.conf:

{
    "files": ["src/Token.sol"],
    "verify": "Token:certora/specs/Token.spec",
    "wait_for_results": "all",
    "msg": "Token verification",
    "rule_sanity": "basic",
    "optimistic_loop": true,
    "loop_iter": 3
}

Run it:

certoraRun certora/conf/Token.conf

Certora sends the job to their cloud prover and gives you a URL to track progress. Results typically come back in 5-30 minutes depending on spec complexity.

Understanding counterexamples

When the Prover finds a violation, it presents a counterexample in the web UI. You'll see:

1. Initial state: Storage values before the transaction
2. Function called: Which function triggered the violation
3. Arguments: Exact values that cause the issue
4. Final state: Storage values after the transaction
5. Assert violated: Which assertion failed

Read counterexamples carefully. Sometimes they're real bugs. Sometimes they're incomplete specs. You forgot a precondition, and the Prover found a technically-valid-but-unreachable scenario. Adding appropriate require statements fixes the latter.

DeFi patterns that matter

Solvency

The most important invariant for any protocol holding user funds:

invariant vaultSolvency()
    underlying.balanceOf(vault) >= vault.totalAssets()
    {
        preserved with (env e) {
            require e.msg.sender != vault;
        }
    }

Access control

Verify that privileged functions are properly gated:

rule onlyAdminCanPause() {
    env e;
    require e.msg.sender != admin();

    pause@withrevert(e);

    assert lastReverted, "Non-admin should not be able to pause";
}

State transitions

Verify that state machines follow valid transitions:

rule validStateTransitions() {
    env e;
    calldataarg args;

    uint8 stateBefore = currentState();

    // Any function call
    method f;
    f(e, args);

    uint8 stateAfter = currentState();

    // Only valid transitions
    assert (stateBefore == 0 && stateAfter == 1) ||  // INIT -> ACTIVE
           (stateBefore == 1 && stateAfter == 2) ||  // ACTIVE -> PAUSED
           (stateBefore == 2 && stateAfter == 1) ||  // PAUSED -> ACTIVE
           (stateBefore == stateAfter),                // No change
        "Invalid state transition detected";
}

Monotonicity

Share prices in vaults should never decrease (absent explicit loss events):

rule sharePriceNonDecreasing() {
    env e;
    calldataarg args;

    uint256 priceBefore = convertToAssets(e, 1000000);

    method f;
    require f.selector != sig:reportLoss(uint256).selector;
    f(e, args);

    uint256 priceAfter = convertToAssets(e, 1000000);

    assert priceAfter >= priceBefore;
}

Limitations and honest takes

Certora isn't perfect. Here's what you should know:

Cost. You need an API key and the Prover runs on their cloud. It's a commercial tool. For serious DeFi work, the cost is justified. For hobbyist projects, consider Halmos as a free alternative.

Timeouts. Complex specs on complex contracts can time out. The Prover has resource limits, and sometimes you'll need to simplify your rules or break them into smaller pieces.

Loop handling. Contracts with unbounded loops are hard to verify. The optimistic_loop setting helps, but it's an approximation. You're trusting that the loop body behavior generalizes.

Learning curve. CVL looks deceptively simple but writing good specs takes practice. Expect to spend a few days getting comfortable before you're productive.

Not a replacement for testing. Certora verifies properties, not behavior. You still need unit tests and fuzz tests alongside manual review. Formal verification is one layer of a defense-in-depth strategy.

Helper contracts

Sometimes you need to expose internal functions or simplify a contract for verification. That's what helper contracts are for:

// certora/helpers/VaultHelper.sol
import "../../src/Vault.sol";

contract VaultHelper is Vault {
    // Expose internal function for verification
    function getInternalAccountingValue() external view returns (uint256) {
        return _internalAccounting;
    }
}

Then verify the wrapper instead of the original:

{
    "files": ["certora/helpers/VaultHelper.sol"],
    "verify": "VaultHelper:certora/specs/Vault.spec"
}

Tips from real audits

1. Start with invariants, not rules. Invariants give you the most bang for your buck. "Total supply == sum of balances" catches a huge class of bugs with one line.

2. Use rule sanity checks. Set "rule_sanity": "basic" in your config. This verifies that your rules aren't vacuously true (passing because the preconditions are unsatisfiable).

3. Name your assertions. Every assert should have a message string. When something fails, you want to know which assertion without staring at line numbers.

4. Iterate quickly. Start with a simple spec, verify it works, then add more rules. Don't write 50 rules and submit them all at once. Debugging will be painful.

5. Read the counterexamples. Half the value of formal verification comes from understanding why a property broke, not just that it broke.

Getting started on your project

Pick one contract. Write three invariants. Run them. Fix any real issues, tighten any vacuous specs. Then expand. You don't need to verify your entire protocol on day one. Start where the money is: the contracts that hold user funds and manage access control.

Get a professional formal verification audit

Try Recon Pro