Formal verification promises something testing cannot: a mathematical proof that a property holds for all possible inputs, not just the ones you thought to try. The Certora Prover delivers that promise through symbolic execution and SMT solving, but the proof is only as strong as the specification you write. A vacuous spec — one that is trivially satisfied because it never actually constrains anything — passes with flying colors and catches nothing.

This article is about writing specs that do real work.

How the Certora Verification Language (CVL) Works

CVL is a declarative specification language that sits on top of Solidity. You write a .spec file that describes the contract’s expected behavior in terms of rules, invariants, and ghost variables. The Certora Prover compiles both the contract bytecode and the spec, builds a mathematical model of all reachable states, and hands that model to an SMT solver (Z3 or CVC5) to check whether the spec is always satisfied.

The key mental model: the prover does not execute code. It reasons about all possible executions simultaneously. When you write a rule, the prover asks “does there exist any assignment of inputs and initial state that violates this property?” If yes, it produces a counterexample. If no such assignment exists, the property is proven for all inputs within the verified scope.

A minimal spec file looks like this:

// SPDX-License-Identifier: MIT
using ERC20 as token;

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function transfer(address, uint256) external returns (bool);
}

rule transferDecreasesBalance(address sender, address recipient, uint256 amount) {
    env e;
    require e.msg.sender == sender;
    require sender != recipient;

    uint256 balanceBefore = balanceOf(sender);
    transfer(e, recipient, amount);
    uint256 balanceAfter = balanceOf(sender);

    assert balanceAfter == balanceBefore - amount,
        "transfer must decrease sender balance by exact amount";
}

The methods block is a dispatch table — it tells the prover which functions exist, their signatures, and whether they depend on env (the transaction context). Marking a method envfree means it does not use msg.sender, msg.value, or block.*, so the prover does not need to universally quantify over all possible environments when calling it. This dramatically reduces the search space and speeds up verification.

Rules vs Invariants vs Hooks

CVL has three primary building blocks. Understanding when to use each is the first design decision in every spec.

Rules

A rule is an imperative-style property. It has a setup phase, calls one or more contract functions, and asserts a post-condition. Rules are the right tool when you want to verify something about a specific transition — what happens when a function is called.

rule noTransferToZeroAddress(uint256 amount) {
    env e;
    address zero = 0;

    transfer@withrevert(e, zero, amount);

    assert lastReverted,
        "transfer to the zero address must always revert";
}

The @withrevert modifier is critical: without it, the prover assumes the call succeeds and skips states where it would revert. Using @withrevert followed by assert lastReverted is the standard pattern for verifying that a function cannot succeed under certain conditions.

Invariants

An invariant is a declarative property that must hold in every reachable state. Unlike a rule, it is not tied to a particular function call — it must survive every operation the contract exposes.

invariant totalSupplyIsSum(address a, address b)
    a != b => balanceOf(a) + balanceOf(b) <= totalSupply()
    {
        preserved {
            requireInvariant totalSupplyIsSum(a, b);
        }
    }

The prover checks invariants in two ways: it verifies the invariant holds in the initial state (after the constructor), and it verifies that if the invariant holds before any function call, it still holds after. This inductive structure is powerful but has a subtle implication: the invariant must be inductively true, not just observationally true. A state might be reachable that satisfies the invariant but from which a subsequent call breaks it — that will be caught. But a state that is unreachable yet technically violates the invariant can cause the prover to raise a spurious counterexample.

The preserved block lets you strengthen the inductive hypothesis by assuming other invariants hold during the proof. Without it, the prover treats each invariant in isolation.

Hooks

Hooks intercept low-level storage operations and let you maintain ghost variables — auxiliary state that exists only in the spec and tracks cumulative information across calls.

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

hook Sstore _balances[KEY address a] uint256 newVal (uint256 oldVal) {
    sumOfBalances = sumOfBalances + newVal - oldVal;
}

invariant sumMatchesTotalSupply()
    sumOfBalances == to_mathint(totalSupply())

This pattern — a ghost variable updated via hooks, then constrained by an invariant — is how you express properties that depend on the aggregate behavior of all accounts. mathint is an unbounded integer type in CVL that avoids overflow issues in the spec itself; always prefer it over uint256 in ghost arithmetic.

Parametric Rules vs Invariants: The Key Distinction

The term “parametric rule” refers to a rule that universally quantifies over which function is called, not just the inputs to a specific function. This is the mechanism for writing properties that must hold across all functions in the contract.

rule balanceNeverExceedsTotalSupply(method f) {
    env e;
    calldataarg args;
    address user;

    require balanceOf(user) <= totalSupply();

    f(e, args);

    assert balanceOf(user) <= totalSupply(),
        "no function should cause a balance to exceed total supply";
}

The method f parameter, combined with calldataarg args, tells the prover: “check this property for every function in the contract’s dispatch table.” The prover will generate a separate verification condition for each method.

When to use an invariant instead: if the property must hold in every state (not just after a specific transition), and especially if you want to use it as a building block for other proofs via requireInvariant, reach for an invariant. If the property is specifically about the change caused by a call — a delta property — use a rule. And if you want to say “for all functions, this delta property holds,” use a parametric rule.

The practical difference matters for the prover’s ability to use properties as lemmas. Invariants can be imported into other invariants and rules via requireInvariant. A parametric rule that has been proven cannot be directly reused as an assumption inside another rule — you would need to re-encode it as an invariant or use a ghost for that purpose.

Specifying Access Control Properties

Access control is one of the most important and easiest classes of property to specify formally. The pattern is clean: for each privileged function, assert that calling it as a non-privileged address always reverts.

methods {
    function owner() external returns (address) envfree;
    function pause() external;
    function setFee(uint256) external;
    function hasRole(bytes32, address) external returns (bool) envfree;
}

definition ADMIN_ROLE() returns bytes32 =
    0x0000000000000000000000000000000000000000000000000000000000000000;

rule onlyOwnerCanPause(address caller) {
    env e;
    require e.msg.sender == caller;
    require caller != owner();

    pause@withrevert(e);

    assert lastReverted,
        "non-owner must not be able to pause the contract";
}

rule onlyAdminCanSetFee(address caller, uint256 newFee) {
    env e;
    require e.msg.sender == caller;
    require !hasRole(ADMIN_ROLE(), caller);

    setFee@withrevert(e, newFee);

    assert lastReverted,
        "non-admin must not be able to set fee";
}

For OpenZeppelin-style role-based access control, the hasRole function is the oracle. The key discipline: always use @withrevert and assert lastReverted. If you forget @withrevert, the prover silently assumes the call succeeded and the rule becomes vacuously true for the revert case.

You can also write the positive direction — the privileged address can perform the action without reverting (assuming other preconditions are met):

rule ownerCanAlwaysPause() {
    env e;
    require e.msg.sender == owner();
    require e.msg.value == 0;
    // Assume contract is not already paused
    require !paused();

    pause@withrevert(e);

    assert !lastReverted,
        "owner should always be able to pause when not already paused";
}

Both directions together form a complete access control spec: the property is exclusive (only the privileged role can call it) and inclusive (the privileged role always can).

Writing Specs for ERC-20 Contracts

A robust ERC-20 spec covers four categories: supply conservation, balance integrity, allowance mechanics, and revert conditions.

using ERC20Token as token;

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function allowance(address, address) external returns (uint256) envfree;
    function totalSupply() 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);
}

ghost mathint ghostTotalSupply {
    init_state axiom ghostTotalSupply == 0;
}

ghost mapping(address => mathint) ghostBalances {
    init_state axiom forall address a. ghostBalances[a] == 0;
}

hook Sstore _totalSupply uint256 newSupply (uint256 oldSupply) {
    ghostTotalSupply = ghostTotalSupply + newSupply - oldSupply;
}

hook Sstore _balances[KEY address a] uint256 newBal (uint256 oldBal) {
    ghostBalances[a] = ghostBalances[a] + newBal - oldBal;
}

// Core conservation invariant
invariant totalSupplyEqualsSumOfBalances()
    ghostTotalSupply == (forall address a. ghostBalances[a])

// Transfer does not change total supply
rule transferPreservesTotalSupply(address to, uint256 amount) {
    env e;
    uint256 supplyBefore = totalSupply();

    transfer(e, to, amount);

    assert totalSupply() == supplyBefore,
        "transfer must not change total supply";
}

// transferFrom reduces allowance correctly
rule transferFromReducesAllowance(
    address owner,
    address spender,
    address recipient,
    uint256 amount
) {
    env e;
    require e.msg.sender == spender;
    require owner != spender;

    uint256 allowanceBefore = allowance(owner, spender);
    require allowanceBefore >= amount;

    transferFrom(e, owner, recipient, amount);

    uint256 allowanceAfter = allowance(owner, spender);

    // Special case: max allowance (type(uint256).max) should not decrease
    assert allowanceBefore == max_uint256
        ? allowanceAfter == max_uint256
        : allowanceAfter == allowanceBefore - amount,
        "allowance must decrease by transfer amount unless it was max";
}

// Integrity: sender cannot spend more than their balance
rule cannotTransferMoreThanBalance(address to, uint256 amount) {
    env e;
    uint256 senderBalance = balanceOf(e.msg.sender);
    require amount > senderBalance;

    transfer@withrevert(e, to, amount);

    assert lastReverted,
        "transfer of more than balance must revert";
}

The max_uint256 special case in transferFromReducesAllowance is a common gotcha. The ERC-20 standard specifies that an allowance equal to type(uint256).max should not be decremented — it acts as an infinite approval. Missing this branch produces a legitimate counterexample.

Writing Specs for ERC-4626 Vaults

ERC-4626 introduces a tightly coupled relationship between shares and assets. The invariant landscape is richer: conversion rates must be monotone, the vault’s asset balance must be consistent with reported total assets, and deposit/withdraw operations must round in favor of the vault (protecting existing shareholders).

using ERC4626Vault as vault;
using ERC20Asset as asset;

methods {
    function totalAssets() external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function convertToShares(uint256) external returns (uint256) envfree;
    function convertToAssets(uint256) external returns (uint256) envfree;
    function maxDeposit(address) external returns (uint256) envfree;
    function deposit(uint256, address) external returns (uint256);
    function withdraw(uint256, address, address) external returns (uint256);
    function redeem(uint256, address, address) external returns (uint256);
    function previewDeposit(uint256) external returns (uint256) envfree;
    function previewWithdraw(uint256) external returns (uint256) envfree;
}

// Rounding direction: deposit must round down (user gets fewer shares)
rule depositRoundsDown(uint256 assets, address receiver) {
    env e;
    uint256 sharesReceived = deposit(e, assets, receiver);
    uint256 assetsConvertedBack = convertToAssets(sharesReceived);

    assert assetsConvertedBack <= assets,
        "shares received must be worth at most the deposited assets";
}

// Rounding direction: withdraw must round up (user burns more shares)
rule withdrawRoundsUp(uint256 assets, address receiver, address owner) {
    env e;
    uint256 sharesBurned = withdraw(e, assets, receiver, owner);
    uint256 assetsConvertedFromShares = convertToAssets(sharesBurned);

    assert assetsConvertedFromShares >= assets,
        "shares burned in withdraw must be worth at least the requested assets";
}

// No free shares: zero assets deposit yields zero shares
rule zeroDepositYieldsZeroShares(address receiver) {
    env e;
    uint256 sharesOut = deposit(e, 0, receiver);
    assert sharesOut == 0,
        "depositing zero assets must yield zero shares";
}

// Atomicity: deposit then immediate redeem returns at most original assets
rule depositRedeemAtMostOriginal(uint256 assets, address user) {
    env e1;
    env e2;
    require e1.msg.sender == user;
    require e2.msg.sender == user;
    // Same block, no intervening state changes
    require e1.block.number == e2.block.number;

    uint256 shares = deposit(e1, assets, user);
    uint256 assetsBack = redeem(e2, shares, user, user);

    assert assetsBack <= assets,
        "round-trip deposit-redeem must not profit the user";
}

The round-trip property (depositRedeemAtMostOriginal) is particularly valuable: it encodes the EIP-4626 invariant that users cannot extract more assets than they deposited in a single atomic sequence, which is the mathematical statement that the vault does not leak value to individual users at the expense of others.

Common Mistakes That Produce Vacuous Proofs

A vacuous proof is a proof of a property that is trivially true — usually because the preconditions are unsatisfiable, meaning there is no state that even reaches the assertion. The prover reports “verified” but has proved nothing meaningful.

Over-constraining with require

// WRONG: This rule is vacuous
rule badTransferRule(address to, uint256 amount) {
    env e;
    require amount > 0;
    require amount < 100;
    require amount > 500; // Contradicts the above — unsatisfiable

    transfer(e, to, amount);
    assert balanceOf(e.msg.sender) >= 0; // Trivially true anyway
}

The prover will verify this instantly because no input satisfies all require statements. The assertion is never reached.

How to detect vacuity: Certora’s tooling has a --rule_sanity flag. Always run specs with --rule_sanity basic or --rule_sanity advanced. It inserts a reachability check — an assert false — at every assertion point. If the prover can prove assert false, the assertion is unreachable and the rule is vacuous.

Asserting Tautologies

// WRONG: Always true regardless of contract behavior
rule tautologyRule(address user) {
    uint256 balance = balanceOf(user);
    assert balance >= 0; // uint256 is always >= 0
}

This is syntactically valid and will always pass, but it says nothing about the contract.

Missing @withrevert on Revert Checks

// WRONG: Without @withrevert, the prover ignores revert paths
rule mustRevertOnOverflow(uint256 a, uint256 b) {
    env e;
    require a + b < a; // Overflow condition

    transfer(e, someAddress, a + b); // No @withrevert

    assert false; // Unreachable in this form — but prover may handle differently
}

Without @withrevert, the prover assumes the function succeeds. Any path on which it would revert is excluded from consideration. The rule may pass not because the function correctly reverts, but because the prover never examined the revert path.

Forgetting the preserved Block on Invariants

When an invariant depends on another invariant being true (for the inductive step to go through), omitting the preserved block with requireInvariant often causes the prover to find spurious counterexamples in intermediate states that are unreachable in practice. Always add requireInvariant for related invariants in the preserved block.

Interpreting Certora Counterexamples

When the prover finds a violation, it generates a counterexample: a concrete assignment of storage values, function inputs, and environment parameters that falsifies the property. Reading it correctly is a skill.

The counterexample report shows:

  • Call trace: the sequence of function calls leading to the violation
  • Storage state: the values of all relevant storage slots before and after each call
  • Assert violated: which specific assertion failed and the values of expressions involved

The first question to ask is: is this a real bug or a spec bug?

Real bugs look like: the prover found an input where balanceOf(sender) decreased by more than amount, or where a non-owner successfully called pause(). The call trace shows a plausible execution.

Spec bugs look like: the counterexample involves storage values that are impossible in a correctly initialized contract (e.g., totalSupply == 0 but some address has balance == 1000), or the environment has msg.sender == address(0). These are artifacts of the inductive proof methodology — the prover considers any initial state, not just reachable ones.

Fix a spec-bug counterexample by adding assumptions to exclude the impossible state:

invariant balanceLeqTotalSupply(address a)
    balanceOf(a) <= totalSupply()
    {
        preserved {
            requireInvariant totalSupplyEqualsSumOfBalances();
        }
    }

Or by constraining the environment:

rule someRule() {
    env e;
    require e.msg.sender != 0; // Exclude impossible zero-sender states
    require e.msg.value == 0;  // No ETH sent to non-payable function
    ...
}

Never add require statements to paper over a real bug. If the counterexample is valid, the property is genuinely violated and the contract has a bug. The temptation to require away inconvenient counterexamples is the single most dangerous failure mode in formal verification workflows.

The Limits of What Certora Can Verify

Understanding where the prover’s guarantees end is as important as knowing how to write specs.

Loop Unrolling

The Certora Prover handles loops by unrolling them a fixed number of times, configured via --loop_iter. With --loop_iter 3, a loop is unrolled three times and the prover checks that any iteration beyond the third cannot be reached (or it marks the rule as potentially unsound with a warning).

// This loop will be checked for up to --loop_iter iterations
for (uint256 i = 0; i < n; i++) {
    balances[recipients[i]] += amounts[i];
}

If n can be arbitrarily large, no finite unrolling proves the property for all n. The prover may return “verified” for the unrolled prefix but this does not constitute a full proof. The Certora report flags this with a LoopIterationReached finding. Treat rules that touch unbounded loops with caution — the proof is partial.

Mitigation: bound the loop variable in the spec, or refactor the contract to operate on a single element per call (a pattern that is also gas-safer on-chain).

External Call Modeling

When a contract makes an external call to an arbitrary address (as in ERC-20’s transferFrom calling an unknown token contract), the prover must model what that external call can do. By default, Certora uses optimistic dispatch or pessimistic dispatch:

  • Pessimistic (default for unresolved calls): the external call can modify any storage, call back into the contract, change balances — anything. This is sound but produces many spurious counterexamples.
  • Optimistic: the external call is assumed to be a no-op or to behave according to a provided summary.

You provide summaries in the methods block:

methods {
    // Assume the external token's transferFrom always succeeds and behaves correctly
    function _.transferFrom(address, address, uint256) external
        => DISPATCHER(true);

    // Or provide a precise summary
    function _.balanceOf(address a) external
        => ghostExternalBalance[a] expect uint256;
}

The DISPATCHER summary tells the prover to only consider known implementations of the function (those in the verification scene). This is appropriate when you control all contracts. For truly external, unknown contracts, the pessimistic model is more honest but harder to work with.

The Halting Problem Boundary

The prover cannot decide all properties of all programs — that is a mathematical impossibility. In practice, the Certora Prover may return TIMEOUT for complex rules on large contracts. This does not mean the property is true or false; it means the SMT problem was too hard to solve in the configured time limit.

Timeout mitigations:

  • Split a large rule into smaller rules
  • Add summarize directives to simplify expensive internal functions
  • Reduce the scope of parametric rules by filtering method f with f.selector != sig:someheavyFunction().selector
  • Use --smt_timeout to allocate more time

What Is Outside Scope

Certora cannot verify:

  • Properties that depend on miners or validators behaving honestly
  • Economic properties that emerge from game theory across multiple independent actors
  • Off-chain components (oracles, keepers, front-ends)
  • Gas costs (there is no gas model)
  • Low-level assembly that cannot be lifted to a symbolic representation

Integrating Certora into an Audit Workflow

Formal verification is most valuable when it is continuous, not a one-time event at the end of development.

Spec as a Design Document

Write specs before writing the implementation, alongside the NatSpec. A spec is a precise statement of intent. If you cannot write the spec, you have not fully specified the behavior. This is the formal-verification analog of test-driven development and has the same clarifying benefits.

Continuous Integration

Add Certora to your CI pipeline using the certora-cli package:

pip install certora-cli

certoraRun \
  src/ERC20.sol \
  --verify ERC20:specs/ERC20.spec \
  --solc solc8.19 \
  --rule_sanity basic \
  --loop_iter 3 \
  --msg "CI run on PR #${PR_NUMBER}"

Run the prover on every pull request. A failing proof on a PR is a signal as important as a failing unit test. Require that all existing rules pass before merging. New functionality should come with new rules.

Spec Review as Part of Audit

During a security audit, the spec itself is an audit artifact. Auditors should:

  1. Review the spec for missing properties: what invariants are not in the spec? What privileged functions are not covered by access control rules?
  2. Check for vacuity: run with --rule_sanity advanced and confirm no rules are vacuous
  3. Trace counterexamples: if the prover found violations that were “fixed” by adding require statements, scrutinize whether those requirements are actually enforced on-chain
  4. Cover the business logic: the most important properties are often not the generic ERC-20 ones (which are well-understood) but the protocol-specific invariants — the accounting identities unique to this vault, this AMM, this lending market

Layering Formal Verification with Fuzzing

Certora and fuzzing (Foundry’s forge fuzz, Echidna, Medusa) are complementary. Fuzzers find bugs quickly and handle loops and external calls naturally. Formal verification provides completeness guarantees in the bounded scope it can handle. A mature workflow runs both:

  • Use fuzzing to find quick wins during development
  • Use Certora to prove the critical invariants that define correctness
  • Any property for which a fuzzer found no violation in 10 million runs but the formal proof is incomplete (due to timeout or loop limits) is in a third category: high confidence but not guaranteed

Prioritizing What to Verify Formally

Not every property needs formal verification. Focus Certora’s compute budget on:

  1. Conservation properties: total supply equals sum of balances, total assets equals sum of depositor claims
  2. Access control: privileged functions are inaccessible to non-privileged callers
  3. No-loss properties: users cannot lose funds through normal operation
  4. Protocol-specific invariants: the mathematical identity that defines your protocol’s correctness (e.g., the AMM invariant x * y == k)

Save unit-test-style checks (revert on zero input, event emitted correctly) for standard tests — formal verification is overkill for those and the prover time is better spent on properties that are hard to test exhaustively.

A Complete Worked Example: Lending Pool Solvency

To close the loop, here is a complete spec for a minimal lending pool’s solvency invariant:

using LendingPool as pool;
using ERC20 as collateralToken;

methods {
    function totalDebt() external returns (uint256) envfree;
    function totalCollateral() external returns (uint256) envfree;
    function debtOf(address) external returns (uint256) envfree;
    function collateralOf(address) external returns (uint256) envfree;
    function collateralFactor() external returns (uint256) envfree; // e.g., 150 = 150%
    function borrow(uint256) external;
    function repay(uint256) external;
    function liquidate(address) external;
    function isHealthy(address) external returns (bool) envfree;
}

ghost mathint ghostTotalDebt {
    init_state axiom ghostTotalDebt == 0;
}

ghost mathint ghostTotalCollateral {
    init_state axiom ghostTotalCollateral == 0;
}

// Solvency: no position can borrow more than collateral * factor
invariant noUndercollateralizedPositions(address user)
    isHealthy(user)
    {
        preserved borrow(uint256 amount) with (env e) {
            require e.msg.sender == user;
            requireInvariant noUndercollateralizedPositions(user);
        }
        preserved liquidate(address target) with (env e) {
            require target != user || !isHealthy(target);
        }
    }

// After liquidation, the liquidated position must be healthy or have zero debt
rule liquidationRestoresHealth(address target) {
    env e;
    require !isHealthy(target); // Position is unhealthy before liquidation

    liquidate(e, target);

    assert isHealthy(target) || debtOf(target) == 0,
        "liquidation must restore health or clear the debt entirely";
}

// Repay always reduces debt
rule repayReducesDebt(uint256 amount) {
    env e;
    address borrower = e.msg.sender;
    uint256 debtBefore = debtOf(borrower);

    repay@withrevert(e, amount);

    bool reverted = lastReverted;

    assert !reverted => debtOf(borrower) < debtBefore,
        "successful repay must strictly reduce debt";
}

// Nobody else's position changes when I borrow
rule borrowDoesNotAffectOthers(uint256 amount, address other) {
    env e;
    require other != e.msg.sender;

    uint256 otherDebtBefore = debtOf(other);
    uint256 otherCollateralBefore = collateralOf(other);

    borrow(e, amount);

    assert debtOf(other) == otherDebtBefore,
        "borrow must not change other users' debt";
    assert collateralOf(other) == otherCollateralBefore,
        "borrow must not change other users' collateral";
}

This spec, combined with --rule_sanity advanced, will detect a wide class of solvency bugs: flash loan attacks that bypass health checks, rounding errors that allow over-borrowing, and liquidation logic that leaves positions in an undefined state.

Conclusion

The Certora Prover is a powerful but demanding tool. Its value is directly proportional to the quality of the specs you feed it. Vacuous proofs, tautological assertions, and missing @withrevert modifiers all produce green checkmarks that provide false confidence. The discipline of formal verification is not in running the tool — it is in writing specs that are both correct (not vacuous) and strong (meaningful enough to rule out real bugs).

Start with conservation invariants and access control rules. Add ghost variables for aggregate state. Use --rule_sanity on every run. Treat every counterexample as a hypothesis to be investigated rather than a nuisance to be suppressed. And integrate the prover into CI so that the spec and the code evolve together — a spec that is six months behind the implementation is worse than no spec at all.

Formal verification does not replace audits or fuzzing. It fills the gap they leave: proving that a specific, precisely stated property holds for all possible inputs, not just the ones anyone thought to try.