CertiK Prover
Login

CertiK Prover user guide

Security properties

A specification is most valuable when it states a security requirement: who may act, what must never change, and what must always add up. This chapter tours the properties you can protect, using one token contract. Each property links to the chapter that covers it in depth.

You will learn
How to turn security requirements into clauses: access control, exact transfers, isolation, conservation, and one-way values, plus the trap of an empty proof.

The token

Token has an owner who mints new tokens, holders who transfer and burn their own tokens, and a totalSupply that must always match the balances. CertiK Prover proves every clause in this file.

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

contract Token {
    address public owner;
    uint256 public totalSupply;
    mapping(address => uint256) public balances;

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

    constructor() {
        owner = msg.sender;
    }

    //@ reverts_when msg.sender != owner;
    //@ ensures balances[to] == \old(balances[to]) + amount;
    //@ ensures totalSupply == \old(totalSupply) + amount;
    //@ assignable balances[to], totalSupply;
    function mint(address to, uint256 amount) external {
        require(msg.sender == owner, "not owner");
        balances[to] += amount;
        totalSupply += amount;
    }

    //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
    //@ ensures balances[to] == \old(balances[to]) + amount;
    //@ assignable balances[msg.sender], balances[to];
    //@ reverts_when to == msg.sender;
    function transfer(address to, uint256 amount) external {
        require(to != msg.sender, "self transfer");
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }

    //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
    //@ ensures totalSupply == \old(totalSupply) - amount;
    //@ assignable balances[msg.sender], totalSupply;
    function burn(uint256 amount) external {
        balances[msg.sender] -= amount;
        totalSupply -= amount;
    }
}

Only the owner can mint

Access control is a revert condition: if the caller is not the owner, mint must fail. Writing it as reverts_when turns the rule into something CertiK Prover checks against the code.

//@ reverts_when msg.sender != owner;
//@ ensures balances[to] == \old(balances[to]) + amount;
//@ ensures totalSupply == \old(totalSupply) + amount;
//@ assignable balances[to], totalSupply;
function mint(address to, uint256 amount) external {
    require(msg.sender == owner, "not owner");
    balances[to] += amount;
    totalSupply += amount;
}

Try it

A missing owner check

The specification says mint reverts for anyone but the owner. Does the code enforce that?

Read-only
//@ reverts_when msg.sender != owner;
//@ ensures balances[to] == \old(balances[to]) + amount;
//@ ensures totalSupply == \old(totalSupply) + amount;
//@ assignable balances[to], totalSupply;
function mint(address to, uint256 amount) external {
    balances[to] += amount;
    totalSupply += amount;
}

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

Transfers move tokens exactly

A transfer must debit the sender and credit the recipient by the same amount, so no tokens appear or vanish. Two ensures clauses state both sides:

//@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
//@ ensures balances[to] == \old(balances[to]) + amount;
//@ assignable balances[msg.sender], balances[to];
//@ reverts_when to == msg.sender;
function transfer(address to, uint256 amount) external {
    require(to != msg.sender, "self transfer");
    balances[msg.sender] -= amount;
    balances[to] += amount;
}

Try it

Tokens out of thin air

This transfer debits the sender and credits the recipient. Do both sides match?

Read-only
//@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
//@ ensures balances[to] == \old(balances[to]) + amount;
//@ assignable balances[msg.sender], balances[to];
function transfer(address to, uint256 amount) external {
    require(to != msg.sender, "self transfer");
    balances[msg.sender] -= amount;
    balances[to] += amount + 1;
}

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

Nobody else is affected

The assignable clause of transfer lists the only balances it may touch, so every other holder is protected:

//@ assignable balances[msg.sender], balances[to];

To state that protection as a condition you can reuse and combine, write it with \forall. Logic and quantifiers explains \forall and ==>:

//@ ensures \forall (address a) a != to ==> balances[a] == \old(balances[a]);

Supply always adds up

Some properties belong to the whole contract rather than one function. An invariant must hold after every transaction; this one says the balances always add up to totalSupply, where \sum_of adds every entry of the mapping:

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

Contract-wide properties covers invariants and \sum_of in depth.

Try it

A burn that skips the books

burn removes tokens from the caller. Do the balances still add up to totalSupply afterwards?

Read-only
//@ invariant \sum_of(balances) == totalSupply;

//@ assignable balances[to], totalSupply;
function mint(address to, uint256 amount) external {
    balances[to] += amount;
    totalSupply += amount;
}

//@ assignable balances[msg.sender], totalSupply;
function burn(uint256 amount) external {
    balances[msg.sender] -= amount;
}

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

Some values only move one way

A constraint compares the end of every successful call with its start. This one, from the capped issuer in Contract-wide properties, says the amount issued never goes down:

constraint totalIssued >= \old(totalIssued);

Beware the empty proof

Every clause is checked only for the starting states your requires clauses allow. If those clauses contradict each other, no state is allowed, nothing is checked, and every clause passes, even a wrong one. CertiK Prover reports this as an ordinary pass.

Try it

A proof about nothing

This specification claims that a withdrawal increases the balance, which is wrong. Why does it pass?

Read-only
//@ requires amount > balances[msg.sender];
//@ requires amount <= balances[msg.sender];
//@ ensures balances[msg.sender] == \old(balances[msg.sender]) + amount;
function withdraw(uint256 amount) external {
    balances[msg.sender] -= amount;
}

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

Before you rely on a pass, make sure your requires clauses can all be true at once. A quick test: break one clause on purpose and confirm that the check now fails.

From requirement to clause

RequirementClause
Only the owner can mintreverts_when msg.sender != owner;
Transfers move tokens exactlyensures balances[to] == \old(balances[to]) + amount;
Nobody else is affectedassignable balances[msg.sender], balances[to];
Supply always adds upinvariant \sum_of(balances) == totalSupply;
A value never decreasesconstraint totalIssued >= \old(totalIssued);

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.