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 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.procps.secp256k1 --version v$(cat deps/k_release)

Poetry dependencies

First you need to set up all the dependencies of the virtual environment using Poetry with the prerequisites python 3.8.*, pip >= 20.0.2, poetry >= 1.3.2:

poetry install

Build using the virtual environment

In order to build kontrol, you need to build these specific targets:

poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry

To change the default compiler:

CXX=clang++-14 poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry

On Apple Silicon:

APPLE_SILICON=true poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry

Targets can be cleaned with:

poetry 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"

For interactive use, spawn a shell with poetry shell (after poetry install), then run an interpreter.

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.