Quick start

You need Node.js 22.12 or newer with npm, on macOS, Linux (x64 or ARM64), or Windows x64.

node --version

CertiK provides the package as a file named certikproject-csol-verifier-<version>.tgz. From the folder that contains it, install it globally with npm:

npm install -g ./certikproject-csol-verifier-<version>.tgz

npm uninstall -g csol-project

csol --version
csol-project --version

Both commands print the package version. The first csol run may download and cache a Java runtime and the Z3 solver, so it needs network access once.

Save this as Counter.sol. The lines that start with //@ are its specification: after a successful call, value has grown by exactly one, the function returns the new value, and nothing else changes. Basics explains where specifications go.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

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

contract Counter {
    uint256 public value;

    //@ ensures value == \old(value) + 1;
    //@ ensures \result == value;
    //@ assignable value;
    function increment() external returns (uint256) {
        value += 1;
        return value;
    }
}

Run csol on the file. CertiK Prover checks every specification and ends with a summary:

csol Counter.sol

… Function 'Counter.increment' verification success. (703ms)
… === Verification Summary: 1 total, 1 passed, 0 failed, 0 errors ===
… Verification success.

Give csol one entry file. It follows that file's imports, so you never list every file:

# Wrong: a directory or a list of files
csol contracts/ Counter.sol Helper.sol

# Right: one entry file; CertiK Prover follows its imports
csol Counter.sol

Scripts and CI can rely on the exit code of csol and csol-project:

When a project has several entry files, list them in csol-project.yaml at the project root. Each entry has an id and the path of its entry file:

schema_version: 1
entrypoints:
  - id: counter
    path: src/Counter.sol

Run csol-project from the project root. It checks each entry with csol and shows live progress:

csol-project

Project: ./csol-project.yaml
Entrypoints: 1 | Prover jobs: 1

Running counter (src/Counter.sol)
✓ counter [1/1]: █ (1.7s, pass: 1, fail: 0, timeout: 0)

No failures or errors.

Exit: 0

Each run saves its results in a new folder under verification-runs/, with one subfolder per entry. Add --jobs 4 to check up to four entries in parallel; csol-project --help lists every option.

verification-runs/csol-project-<timestamp>-<pid>/
├── summary.json
└── 0001-counter/
    ├── result.json
    ├── events.jsonl
    └── stderr.log

CertiK invites you to CertiK Account by email. Follow the link to create your account, or sign in if you already have one. The invitation adds you to your organization, and your organization is what CertiK grants access to.

Open CertiK Prover, select Login, then Continue with CertiK Account. If you belong to several organizations, choose the one CertiK invited you to.

After sign-in, the Projects page lists each verified project with its latest outcome. If it shows No accessible projects, ask your CertiK contact to grant your organization access.

On the project page, open Results for a finished task to see every entry and its outcome. Each failed specification comes with its counterexample.