Kontrol Cheatsheet

Cheatsheet with (almost) all Kontrol options and gotchas
This cheatsheet provides a comprehensive list of options for conducting Kontrol verification of smart contracts, along with additional information about the K ecosystem.

kontrol commands

These commands encompass all the functionality involved in the verification process, from building your project into a full-fledged K definition to examining the verification output of a symbolic run in detail.
Make K definitions from a Foundry project
kontrol build
Symbolically execute provided tests
kontrol prove --test TestContract.testName
List all proof files with their status
kontrol list
Statically print a proof
kontrol show ContractTest.testName
Show a proof in the KCFG visualizer
kontrol view-kcfg ContractTest.testName
You can extensively customize the above commands to meet your specific verification requirements using the following flags.

kontrol build

Make K definitions from a Foundry project with build.

build Flags

There are flags available for the build stage that allow you to change the set of lemmas used for reasoning and specify the desired behavior for rebuilding or re-executing symbolic tests.
Verbose build trace
--require $lemmas
Include a file of $lemmas when forming the K definition
--module-import $module
A $module from the $lemmas file provided in the above flag.
Note: $module must be of the form TestContract:ModuleName
Will rebuild the K definition, even if it was previously built

Example of Chaining build Flags

Let's look at what a typical kontrol build example may look like. You will likely have the following contents:
File Name
File Path
Custom Lemma
A module you want Kontrol to include in its reasoning
Symbolic properties
For this example, we will assume that you have already run kontrol build once and this is not your first time symbolically executing the properties. You have also identified the necessary lemmas and included them in MYPROJECT-LEMMAS.
To symbolically execute your properties using the fastest available backend (booster backend), you will need to rekompile the K definition of the project. To do this your command will look like this:
kontrol build --require test/myproject-lemmas.k \
--module-import MyProperties:MYPROJECT-LEMMAS \

kontrol prove

Symbolically execute provided tests with prove.


These flags specify what you prove and how you prove it. The flags include: the backend used for symbolic execution, the new lemmas to include for symbolic reasoning, resource distribute and other potential changes.
--test $testName
Specifies the name of the test function to symbolically execute. Multiple flags can be provided for parallel execution with different functions.
Restarts symbolic execution instead of resuming from the last saved run.
--bmc-depth $n
Enables bounded model checking, unrolling all loops to a maximum depth of $n .
Uses the booster backend (faster) instead of the legacy backend.
--smt-timeout $ms
Sets the timeout in milliseconds for SMT queries.
--smt-retry-limit $n
Specifies the number of times to retry SMT queries with scaling timeouts.
--smt-tactic $smt_tactic
Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)
Abstract any gas-related computations, provided the cheatcode infiniteGas was enabled. This simplifies and speeds up symbolic execution.
Does not store a node for every EVM call made.
--workers $n
Sets the number of parallel processes run by the prover. It should be at most (M - 8) / 8 in a machine with M GB of RAM.
--max-depth $n
Sets the maximum number of K steps before the state is saved in a new node in the KCFG.
--max-iterations $n
Sets the number of times to expand the next pending node in the KCFG.
--bug-report $name
Generates a bug report with the given name.
Generates and shows the counterexample, which refers to the test parameter values that lead to a failing test.
Stop execution on other branches if a failing node is detected.

Example of Chaining prove Flags

Let's look at what a typical kontrol prove example may look like. For this example we will assume the following scenario:
  • There are two symbolic properties to execute in parallel.
    • testMyProperty1
    • testMyProperty2
    • Both are in a contract named MyProperties
  • There are loops present in the code, and before providing invariants for those we want to use the simpler approach of bounded model checking, unrolling the loops only up to 10 iterations
  • We want to allow the SMT solver enough time to reason
  • We want to achieve maximum speed of symbolic execution. This is possible with the following tweaks:
    • Don't allocate any resources to gas computations, since these are costly and can cause numerous branching
    • Create as few nodes as possible, since this saves on writing time. In particular, don't produce any nodes when making EVM calls
    • Use the fastest symbolic execution backend available, the booster backend
The command to execute testMyProperty1 and testMyProperty2, with that set of characteristics is the following:
kontrol prove --test MyProperties.testMyProperty1 \
--test MyProperties.testMyProperty2 \
--bmc-depth 10 \
--smt-timeout 10000 \
--auto-abstract-gas \
--no-break-on-calls \
--workers 2 \

To make use of for all kontrol options, it is recommended you use a bash script that simplifies parameter tweaking and allows for a better verification experience. It is also recommended you save the output of running kontrol to a file for easier inspection and debugging.
Here is a template to have better control over kontrol. To save the output of running a template run-kontrol.sh to log.out , from the root directory of a Foundry project, you can use the following command:
time bash test/run-kontrol.sh 2>&1 | tee log.out
To interpret the result of running this script, please refer to K Control Flow Graph (KCFG).


set -euxo pipefail
kontrol_build() {
kontrol build \
--verbose \
--require ${lemmas} \
--module-import ${module} \
${rekompile} \
kontrol_prove() {
kontrol prove \
--max-depth ${max_depth} \
--max-iterations ${max_iterations} \
--smt-timeout ${smt_timeout} \
--bmc-depth ${bmc_depth} \
--workers ${workers} \
${reinit} \
${bug_report} \
${break_on_calls} \
${auto_abstract} \
${tests} \
# kontrol build options
# kontrol prove options
# break_on_calls=
# auto_abstract=
# use_booster=
# List of tests to symbolically execute
tests+="--test MyProperties.testMyProperty1 "
tests+="--test MyProperties.testMyProperty2 "
pkill kore-rpc || true