Certora Examples

Summarization is a core feature of the Certora Prover used to simplify complex verification tasks. It enables:

1. Reasoning about external calls: Representing the behavior of external contracts or calls without verifying their full implementation.
2. Modular verification: Splitting a large verification problem into multiple independent subproblems by using symbolic representations of specific parts.
3. Interface point checking: Verifying properties at the boundaries of contract interfaces.

For detailed technical specifications, refer to the official Certora documentation on summaries.

This repository provides a comprehensive collection of examples for the Certora Verification Language (CVL). These examples cover a wide range of CVL commands, from basic assertions to advanced concepts like ghost variables, storage access, and summarization. They are categorized by command type and include real-life code snippets and specifications that have been used to identify critical bugs in smart contracts.

For a complete guide and full documentation, refer to the official Certora documentation at https://docs.certora.com.

This example demonstrates how to verify smart contracts using transient storage fields (introduced in recent EVM updates). It uses a contract named TransientTest that implements a simple lock mechanism using a transient boolean field.

Key verification techniques shown in this example include:

• Using Tstore and Tload hooks to intercept accesses to transient fields.
• Performing direct storage access from CVL on transient fields.

This repository serves as a collection of practical examples demonstrating how to use the Certora Verification Language (CVL). The specifications provided in this repository are compatible with CVL2.

Use these examples to learn how to write formal specifications for smart contracts and how to interact with the Certora Prover.

In Certora Verification Language (CVL), you can use address type variables to call methods on contracts. This enables dynamic dispatch, where the specific function call is resolved based on the actual contract implementation associated with the address at runtime. This is useful for specifying properties that must hold true regardless of which contract is being interacted with via an address variable.

using A as a;
using B as b;

rule AddressCall {
    env e;
    address x;
    // x.foo(e) calls the 'foo' function on the contract at address x
    assert x.foo(e) >= 1 && x.foo(e) <= 2;
}

In Certora Verification Language (CVL), an invariant must be 'strong' enough to cover all reachable states from the initial state. If an invariant is too weak, the Certora Prover may find a counterexample by starting from an arbitrary state that satisfies the invariant but allows a transition to a state that violates it.

In the BallGame example:

• Weak Invariant: playerTwoNeverReceivesBall only assumes player 2 does not have the ball. However, if the ball starts with player 4, a pass call can move the ball to player 2, violating the invariant.
• Strong Invariant: BallGameCorrect.spec fixes this by explicitly defining the allowed set of states (e.g., the ball must be held by either player 1 or player 3), ensuring the Prover only considers valid starting configurations.

Ghost elements are used to model state or logic that does not exist in the Solidity code but is necessary for verification.

• Ghost Variables: Can be simple variables or ghost mappings.
• Ghost Functions: CVL functions used to compute values for verification.
• init_state: Used to define the initial state of ghost variables.
• axiom: Used to define truths about ghost variables that the prover can assume.
• Ghost Summary: Summaries that describe the effects on ghost state.

You can use different keywords to control how the Certora Prover treats function returns:

1. ALWAYS(x): Forces the function to return exactly x. Any rule asserting a different value will fail.
2. CONSTANT: Asserts that the function returns the same value every time it is called within a transaction, but the Prover is free to choose any value for that constant.
3. NONDET: Asserts that the function returns a non-deterministic value. Note that using NONDET to imply no state change can be unsound if the actual implementation could change storage.

Example of ALWAYS vs CONSTANT behavior:

• If get1 is ALWAYS(7) and get2 is CONSTANT, get2 will always return the same value, but that value might not be 7.

The TransientStorage example demonstrates how to reason about smart contracts that use the new Ethereum opcodes tstore and tload for reentrancy guards (e.g., using a MockMutexer contract).

To verify properties involving these opcodes, Certora provides specific CVL hooks:

• ALL_TSTORE: A hook used to reason about all tstore operations.
• ALL_TLOAD: A hook used to reason about all tload operations.

These hooks allow the prover to model the behavior of transient storage, which is essential for verifying guards that rely on this new storage type.

The viewReentrancy builtin rule is used to detect vulnerabilities where a contract's state is inconsistent during a view function call due to an ongoing reentrant call.

In the provided examples, ViewReentrancy.spec demonstrates that even if a contract uses a standard reentrancy guard (like in BankGuardFix.sol), the rule can still be violated if the guard does not protect third parties that rely on view functions during the reentrant window.