Kontrol
  • Overview
    • Kontrol
      • The significance
      • Installations
  • Guides
    • Proofcast Episode: Getting Started
    • Kontrol Example
      • Property Verification using Kontrol
      • K Control Flow Graph (KCFG)
      • Proof Management
      • Debugging a Proof
    • Node Refutation
    • Bytecode Verification
    • Advancing Proofs
      • KEVM Lemmas
      • Writing Simplifications
      • Rule Application
      • Symbolic Storage
  • Cheatsheets
    • Kup Cheatsheet
    • Kontrol Cheatsheet
    • Cheatcodes
  • Tips
    • Debugging Failing Proofs
  • Glossary
    • Kontrol Arguments
    • Kontrol Build Options
    • Kontrol Prove Flags
  • Developer Docs
    • Digest File
  • Learn More
    • Resources
    • Example Projects
  • 🔗Links
    • Join our Discord!
    • Kontrol Repo
    • Gitbook Repo
Powered by GitBook
On this page
  • System Requirements
  • Installing Foundry
  • Installing Kontrol

Was this helpful?

Edit on GitHub
  1. Overview
  2. Kontrol

Installations

Everything you need to install

System Requirements

Before installing Kontrol, ensure your system meets the following requirements:

  • RAM: 16GB of RAM is recommended for running Kontrol effectively

  • SWAP Space: 16GB of SWAP space is recommended for installation and operation

    • On Linux systems, you can check your current SWAP space with free -h

    • To increase SWAP space, you can create a swap file:

      sudo fallocate -l 16G /swapfile
      sudo chmod 600 /swapfile
      sudo mkswap /swapfile
      sudo swapon /swapfile

      To make the SWAP file permanent, add this line to /etc/fstab:

      /swapfile none swap sw 0 0

Users running WSL (Windows Subsystem for Linux) should note that WSL allocates only 2GB of RAM by default. This is insufficient for Kontrol. You'll need to increase the memory allocation in your WSL configuration file (.wslconfig) to at least 16GB.

Installing Foundry

To install Foundry execute the following command:

curl -L https://foundry.paradigm.xyz | bash

After installation open a new terminal session or reload your PATH and run foundryup.

Installing Kontrol

bash <(curl https://kframework.org/install)

After installing kup, open a new terminal session or reload your PATH and install Kontrol using kup with the following command:

kup install kontrol

The first installation of kup will take sometime. Check out the Kup Cheatsheet for some additional information!

Docker Installation

Kontrol is also available as a Docker image, which can be used to run Kontrol without installing it on your host system. This is particularly useful for CI/CD pipelines or when you want to avoid local installation.

To use the Kontrol Docker image:

# Pull the latest version
docker pull runtimeverificationinc/kontrol

CI Installation

name: Kontrol CI
on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
      - uses: actions/setup-node@v3
        with:
          node-version: '18'
      - uses: foundry-rs/foundry-toolchain@v1
      - uses: runtimeverification/install-kontrol@v1
      - name: Run Kontrol
        run: kontrol prove

This action handles the installation of all required dependencies and sets up Kontrol in your CI environment.

PreviousThe significanceNextProofcast Episode: Getting Started

Last updated 1 month ago

Was this helpful?

For other installation methods, go to the .

The simplest way to install Kontrol is with the kup. To install kup execute the following command:

The Docker image includes all necessary dependencies and is automatically updated with each Kontrol release. You can find all available versions on .

For GitHub Actions workflows, you can use the official action. Here's an example workflow:

For detailed instructions on building Kontrol from source, go to the .

Foundry Documentation
package manager
Docker Hub
install-kontrol
Kontrol repository