CertiK Prover user guide

Where specifications live

You write specifications inside your Solidity files, in comments that start with //@. The Solidity compiler ignores them, so the deployed contract does not change; CertiK Prover reads them and checks the code against them.

You will learn: The two comment forms, where each kind of specification goes, and how CertiK Prover finds them.
Builds on: Quick start

Specification comments

There are two ways to write a specification comment. Both hold the same clauses, and every clause ends with a semicolon.

One line: `//@`

Start the line with //@ followed by a space. Write one clause per line.

//@ ensures value == \old(value) + 1;

A block: `/@ … @/`

Put several clauses between /*@ and @*/. Like a line comment, the block describes the declaration that follows it.

/*@
  ensures \result == n * (n + 1) / 2;
  assignable \nothing;
@*/
function triangle(uint256 n) external pure returns (uint256) {

Specification comments never change what the contract does. solc compiles the file exactly as before, and the deployed bytecode is identical.

Where to put them

A specification describes whatever it sits directly above. This contract uses all three positions, and CertiK Prover proves every clause in it.

Bank.sol

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

contract Bank {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

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

    //@ ensures balances[msg.sender] == \old(balances[msg.sender]) + msg.value;
    //@ assignable balances[msg.sender], totalDeposits;
    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    /*@
      ensures \result == n * (n + 1) / 2;
      assignable \nothing;
    @*/
    function triangle(uint256 n) external pure returns (uint256) {
        uint256 total = 0;
        //@ maintaining 1 <= i && i <= n + 1;
        //@ maintaining total == (i - 1) * i / 2;
        //@ decreasing n + 1 - i;
        //@ assigning i, total;
        for (uint256 i = 1; i <= n; i++) {
            total += i;
        }
        return total;
    }
}

Position	Clauses	What it describes
Directly above a function (lines 10–11, 17–20)	`requires`, `ensures`, `assignable`, revert clauses	One call of that function. Your first specification teaches these clauses.
In the contract body, outside any function (line 8)	`invariant`	The whole contract, between transactions: here, the recorded balances always add up to `totalDeposits`. Contract-wide properties teaches these clauses.
Directly above a loop (lines 23–26)	`maintaining`, `decreasing`, `assigning`	Every repetition of the loop. Loops teaches these clauses.

For now, notice that each clause sits directly above what it describes.

Read a clause

Every clause has the same three parts.

//@ ensures value == \old(value) + 1;

Keyword

ensures says what kind of claim this is.

Condition

value == \old(value) + 1 is a true-or-false expression, written like Solidity.

Semicolon

; ends the clause.

Conditions use Solidity operators and the contract's own names. They cannot change state, so write ==, never =. Names that start with a backslash, such as \old and \result, are specification built-ins; the next chapter introduces them.

How CertiK Prover finds them

CertiK Prover starts from the entry file you give it, follows its imports, and checks every specification in the resulting project. A function without a specification is still compiled with the project, but its specification is what tells CertiK Prover what to prove.

Common mistake: no space after `//@`

Without the space, the line is an ordinary comment and CertiK Prover never sees the clause. This check passes, even though increment adds 1, not 2:

//@ensures value == \old(value) + 2;
function increment() external {
    value += 1;
}

Always write //@ followed by a space. If a result looks too good, confirm that every clause starts with //@ .

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.

One line: //@