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
  • Create a new Foundry project
  • Install Kontrol cheatcodes

Was this helpful?

Edit on GitHub
  1. Guides

Kontrol Example

How to run property tests with Kontrol

PreviousProofcast Episode: Getting StartedNextProperty Verification using Kontrol

Last updated 22 days ago

Was this helpful?

Create a new Foundry project

forge init kontrolexample

This command creates a new Foundry project that serves as an example. The project's structure is explained in detail in the . Currently, we can only perform fuzzing on parametric tests because the project is not configured to support symbolic execution. We will discuss this topic later in Property Verification using Kontrol. With the project created, we will install Kontrol cheatcodes and then begin editing the code.

Install Kontrol cheatcodes

To use Kontrol cheatcodes, we need to install a required for symbolic execution. First, navigate into the project directory. Then you can install it with Foundry by running the following command:

forge install runtimeverification/kontrol-cheatcodes

These cheatcodes enable us to generalize the storage of an Ethereum account by making it symbolic or by allowing any type of call, such as a .

A similar effect can be achieved by running kontrol init instead of forge init. This command initializes a new Foundry project with the Kontrol cheatcodes already installed and a kontrol.toml configuration file automatically created.

You can add a kontrol.toml file and Kontrol cheatcodes to an existing project by running kontrol init --skip-forge.

With the project created and the Kontrol cheatcodes installed we can begin editing the code.

Foundry book
new Solidity library
delegatecall