CertiK Prover user guide

Quick reference

Every specification form this guide teaches, what it means, where you write it, and the chapter that explains it.

Writing specifications

Form	Meaning	Where	Learn more
`//@ clause;`	One specification line. The space after `//@` is required.	Directly above what it describes	Basics
`/@ clause; clause; @/`	Several clauses in one comment block.	Directly above what it describes	Basics

Function clauses

Form	Meaning	Where	Learn more
`requires P;`	A condition callers must guarantee. It is assumed while the function is checked and proved at every call.	Above a function	Your first specification
`ensures P;`	A condition that holds when the function returns successfully.	Above a function	Your first specification
`assignable x, m[k];`	The only storage the function may change; everything else stays the same.	Above a function	Your first specification
`reverts_when P;`	If `P` holds at the start, the call reverts.	Above a function	Your first specification
`reverts_only_when P;`	If the call reverts, `P` held at the start.	Above a function	Your first specification
`reverts_when_and_only_when P;`	The call reverts exactly when `P` holds at the start.	Above a function	Your first specification
`also`	Starts another case. Every case whose `requires` holds must be satisfied.	Above a function	Cases and modifiers
`let (T x) = E;`	Captures a value once, before the cases start.	Above a function	Cases and modifiers

Inside conditions

Form	Meaning	Where	Learn more
`\old(e)`	The value of `e` when the call started.	Inside any condition	Your first specification
`\result`	The value the function returns.	In `ensures`	Your first specification
`\nothing`	No storage may change.	In `assignable`	Your first specification
`P ==> Q`	If `P` holds, `Q` must hold.	Inside any condition	Logic and quantifiers
`P <==> Q`	`P` and `Q` are both true or both false.	Inside any condition	Logic and quantifiers
`\forall (T x) P`	`P` holds for every value `x` of type `T`.	Inside any condition	Logic and quantifiers
`\exists (T x) P`	`P` holds for at least one value `x` of type `T`.	Inside any condition	Logic and quantifiers
`a + b`	Exact integer arithmetic (`mathint`): it never overflows or wraps.	Inside any condition	Logic and quantifiers
`\sum_of(m)`	The sum of every numeric entry of a mapping or array; `\sum_of(a[i:j])` sums a range.	Inside any condition	Contract-wide properties

Contract-wide properties

Form	Meaning	Where	Learn more
`invariant P;`	Holds before and after every top-level transaction.	In the contract body	Contract-wide properties
`constraint P;`	Holds when a public or external call returns, comparing with its start through `\old`.	In the contract body	Contract-wide properties
`always P;`	Holds whenever any function starts or finishes.	In the contract body	Contract-wide properties
`\prev_tx(x)`	The value of `x` after the previous transaction.	In an `invariant`	Contract-wide properties

Modifiers

Form	Meaning	Where	Learn more
`establishes P;`	Holds just before `_` runs the wrapped function.	Above a modifier	Cases and modifiers
`expects P;`	Holds just after the wrapped function returns to `_`.	Above a modifier	Cases and modifiers

Loops

Form	Meaning	Where	Learn more
`maintaining P;`	Holds before the first repetition and after every repetition.	Above a loop	Loops
`assigning x, y;`	The only variables the loop may change. Required on every loop.	Above a loop	Loops
`decreasing e;`	Shrinks on every repetition and never goes below zero, so the loop ends.	Above a loop	Loops

Commands

Form	Meaning	Where	Learn more
`csol File.sol`	Checks one entry file and every file it imports.	Terminal	Quick start
`csol-project`	Checks every entry listed in `csol-project.yaml`.	Terminal	Quick start
`exit 0 · 1 · 2 · 3`	Passed · counterexample found · error · inconclusive.	Terminal	Quick start

Run the full examples

Every form on this page appears in a complete, verified example in the CertiK Prover Server Tutorial project, organized by chapter under user-guide/. Sign in to open it.