CertiK Prover user guide

Contract-wide properties

Some rules belong to the whole contract rather than to one function: a cap that is never exceeded, a total that always matches, a counter that never goes back. You write them once in the contract body, and CertiK Prover checks them against every function.

You will learn: invariant, constraint, always, \prev_tx, and \sum_of.
Builds on: Security properties and Logic and quantifiers

A capped issuer

CappedIssuer issues units up to a cap fixed at deployment. Its contract-wide properties sit in one /*@ … @*/ block in the contract body:

CappedIssuer.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract CappedIssuer {
    uint256 public immutable cap;
    uint256 public totalIssued;

    /*@
      invariant totalIssued <= cap;
      invariant totalIssued >= \prev_tx(totalIssued);
      constraint totalIssued >= \old(totalIssued);
      always totalIssued <= cap;
    @*/

    constructor(uint256 initialCap) {
        cap = initialCap;
    }

    //@ ensures totalIssued == \old(totalIssued) + amount;
    //@ assignable totalIssued;
    //@ reverts_when_and_only_when amount > cap - totalIssued;
    function issue(uint256 amount) external {
        require(amount <= cap - totalIssued, "cap exceeded");
        totalIssued += amount;
    }
}

Four forms

Each form is checked at different moments:

Form	Checked	Use it for
`invariant P;`	Before and after every top-level transaction.	Facts that hold whenever the contract is at rest, such as caps and totals.
`constraint P;`	When a public or external call returns successfully, with `\old` meaning the start of that call.	How one call may change state, such as a value that never decreases.
`always P;`	Whenever any function starts or finishes, including internal ones.	Facts that must hold even partway through a transaction.
`\prev_tx(x)`	Inside an `invariant`: the value after the previous transaction.	Comparing one transaction with the one before it.

A top-level transaction is the outermost call from outside the contract. While it runs, an invariant may be briefly false, as long as it holds again when the transaction ends. Use always when a fact must hold at every function boundary.

Invariants: true between transactions

The constructor must establish each invariant, and every function must preserve it. CertiK Prover checks this inductively: assuming the invariant holds before a call, it must hold after the call.

8//@ invariant totalIssued <= cap;
9
10constructor(uint256 initialCap) {
11    cap = initialCap;
12}
13
14//@ assignable totalIssued;
15function issue(uint256 amount) external {
16    totalIssued += amount;
17}

Select Run CertiK Prover to check this code against its specification.

Constraints: how one call may change state

An invariant sees only the current state, so it cannot say "never decreases". A constraint can, because \old refers to the start of the call. In this playground the invariant holds, yet the constraint catches a bug.

8/*@
9  invariant totalIssued <= cap;
10  constraint totalIssued >= \old(totalIssued);
11@*/
12
13constructor(uint256 initialCap) {
14    cap = initialCap;
15}
16
17//@ assignable totalIssued;
18function issue(uint256 amount) external {
19    require(amount <= cap - totalIssued, "cap exceeded");
20    totalIssued = amount;
21}

Select Run CertiK Prover to check this code against its specification.

\prev_tx(x) makes the same comparison across transactions instead of within one call. The capped issuer uses it to say the total never shrinks from one transaction to the next:

invariant totalIssued >= \prev_tx(totalIssued);

Totals across a collection: `\sum_of`

\sum_of adds up the numeric entries of a mapping or array, so an invariant can tie a whole collection to a running total. This is the supply invariant from Security properties:

//@ invariant \sum_of(balances) == totalSupply;

A range selects part of an array: \sum_of(values[0:i]) adds the first i entries. Loops uses that form in a loop invariant.

\sum_of exists only in the specification. It adds no loop and no storage to the contract.

Run the full examples

Every code sample and playground on this page is a complete contract in the CertiK Prover Server Tutorial project, where CertiK Prover runs it on the server. Sign in and open an entry's results to see the real run behind each simulated one.