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.

Command	Description	Example
build	Make K definitions from a Foundry project	kontrol build
prove	Symbolically execute provided tests	kontrol prove --test TestContract.testName
list	List all proof files with their status	kontrol list
show	Statically print a proof	kontrol show ContractTest.testName
view-kcfg	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.

Flag	Description
--verbose	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
--rekompile	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:

Content	File Name	File Path
Custom Lemma	myproject-lemmas.k	test/myproject-lemmas.k
A module you want Kontrol to include in its reasoning	MYPROJECT-LEMMAS	test/myproject-lemmas.k
Symbolic properties	MyProperties

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 \
               --rekompile

---

kontrol prove

Symbolically execute provided tests with prove.

Flags

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.

Flag	Description
--test $testName	Specifies the name of the test function to symbolically execute. Multiple flags can be provided for parallel execution with different functions.
--reinit	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 .
--use-booster	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)
--auto-abstract-gas	Abstract any gas-related computations, provided the cheatcode infiniteGas was enabled. This simplifies and speeds up symbolic execution.
--no-break-on-calls	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.
--counterexample-information	Generates and shows the counterexample, which refers to the test parameter values that lead to a failing test.
--fail-fast	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                         \
              --use-booster

---

Recommended Workflow

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).

Script

#!/bin/bash

set -euxo pipefail

kontrol_build() {
    kontrol build                     \
            --verbose                 \
            --require ${lemmas}       \
            --module-import ${module} \
            ${rekompile}              \
            ${llvm_library}
}

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}                           \
            ${use_booster}
}

###
# kontrol build options
###
lemmas=test/myproject-lemmas.k
base_module=MYPROJECT-LEMMAS
module=MyProperties:${base_module}

rekompile=--rekompile
#rekompile=

###
# kontrol prove options
###
max_depth=10000

max_iterations=10000

smt_timeout=100000

bmc_depth=10

workers=2

reinit=--reinit
reinit=

break_on_calls=--no-break-on-calls
# break_on_calls=

auto_abstract=--auto-abstract-gas
# auto_abstract=

bug_report=--bug-report
#bug_report=

use_booster=--use-booster
# use_booster=

# List of tests to symbolically execute
tests=""
tests+="--test MyProperties.testMyProperty1 "
tests+="--test MyProperties.testMyProperty2 "

pkill kore-rpc || true
kontrol_build
kontrol_prove