Kontrol

Kontrol combines KEVM and Foundry to grant developers the ability to perform formal verification without learning a new language or tool. This is especially useful for those who are not verification engineers. Additionally, developers can leverage Foundry test suites they have already developed and use symbolic execution to increase the level of confidence.

Documentation & Support

Documentation for Kontrol can be found in Kontrol book.

Join our Kontrol Telegram Group or Discord server if you have any questions or require support.

Fast Installation

• bash <(curl https://kframework.org/install): install kup package manager.
• kup install kontrol: install Kontrol.
• kup list kontrol: list available Kontrol versions.

NOTE: The first run will take longer to fetch all the libraries and compile sources. (30m to 1h)

Build from source

K Framework

You need to install the K Framework on your system, see the instructions there. The fastest way is via the kup package manager, with which you can do to get the correct version of K:

kup install k.openssl.secp256k1 --version v$(cat deps/k_release)

uv

Setting up Python dependencies and the virtual environment is done using uv. You can either install uv directly or use the nix develop shell:

nix develop
uv sync
exit # exit nix develop shell

Build using the virtual environment

In order to build kontrol, you need to build these specific targets. Note that you can use kontrol.base (without keccak or aux lemmas), kontrol.aux (with aux lemmas), kontrol.keccak (with keccak lemmas) and kontrol.full (with all lemmas) instead of kontrol.* (which builds them all).

uv run kdist --verbose build -j2 "kontrol.*"

To change the default compiler:

CXX=clang++-14 uv run kdist --verbose build -j2 "kontrol.*"

On Apple Silicon:

APPLE_SILICON=true uv run kdist --verbose build -j2 "kontrol.*"

Targets can be cleaned with:

uv run kdist clean

For more information, refer to kdist --help.

For developers

Use make to run common tasks (see the Makefile for a complete list of available targets).

• make build: Build wheel
• make check: Check code style
• make format: Format code
• make test-unit: Run unit tests

To update the expected output of the tests, use the --update-expected-output flag:

make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output"

The full run takes hours, so the Update Expected Output workflow can do it on a CI runner instead. Dispatch it against your branch, then apply the result:

gh run download <run-id> --name expected-output --dir src/tests/integration/test-data/show
git add src/tests/integration/test-data/show && git commit -m 'Update expected output files'

The artifact expires after 7 days.

Build Kontrol with Kup and Specific Dependency Overrides

---

This is relevant for internal development to build a custom version of Kontrol against unreleased upstream dependencies. See KUP docs for more information

Using Kup

---

Relevant dependency options are shown below and can be listed using kup list kontrol --inputs
For example:

Inputs:
├── k-framework - follows kevm/k-framework
├── kevm - github:runtimeverification/evm-semantics (6c2526b)
│   ├── blockchain-k-plugin - github:runtimeverification/blockchain-k-plugin (c9264b2)
│   │   ├── k-framework - github:runtimeverification/k (5d1ccd5)
│   │   │   ├── haskell-backend - github:runtimeverification/haskell-backend (d933d5c)
│   │   │   │   └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
│   │   │   ├── llvm-backend - github:runtimeverification/llvm-backend (37b1dd9)
│   │   │   │   ├── immer-src - github:runtimeverification/immer (4b0914f)
│   │   │   │   └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
│   │   │   └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
│   │   └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/rv-utils
│   ├── haskell-backend - follows kevm/k-framework/haskell-backend
│   ├── k-framework - github:runtimeverification/k (81bcc24)
│   │   ├── haskell-backend - github:runtimeverification/haskell-backend (786c780)
│   │   │   └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
│   │   ├── llvm-backend - github:runtimeverification/llvm-backend (d5eab4b)
│   │   │   ├── immer-src - github:runtimeverification/immer (4b0914f)
│   │   │   └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
│   │   └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
│   └── rv-utils - follows kevm/k-framework/rv-utils
└── rv-utils - follows kevm/rv-utils

Notice: the 'follows' in the 'kup list' output. This shows the links to the important dependencies and which are affected when you set the overrides.

Now run a build using kup and specific dependency overrides:

kup install kontrol --override kevm/k-framework/haskell-backend "hash/branch_name" --override kevm/k-framework/haskell-backend "hash"

Note: It's important that you use the short-rev hash or the long for specific revisions of the dependencies to modify.

Example to fetch the desired hash to insert a different dependency version into the kontrol build. Substitude the k-framework revision used to build kontrol.

K_TAG=$(curl -s https://raw.githubusercontent.com/runtimeverification/kontrol/master/deps/k_release)
git ls-remote https://github.com/runtimeverification/k.git refs/tags/v${K_TAG} | awk '{print $1}'

Resources

• KEVM: Formal model of EVM in K Framework.
• EVM Yellowpaper: Original specification of EVM.

For more information about the K Framework, refer to these sources:

• The K Tutorial
• Semantics-Based Program Verifiers for All Languages
• Reachability Logic Resources
• Matching Logic Resources
• Logical Frameworks: Discussion of logical frameworks.