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
  • Getting Started
  • Community

Was this helpful?

Edit on GitHub
  1. Overview

Kontrol

Kontrol your smart contracts with formal verification made simple

NextThe significance

Last updated 5 days ago

Was this helpful?

is a powerful formal verification tool for EVM smart contracts that makes complex verification easy. Kontrol seamlessly integrates with Foundry's testing framework, allowing developers to utilize existing Foundry tests as formal specifications. This approach simplifies the verification process, making it accessible even to those without a background in formal verification.

  • Open Source: Kontrol is open source under the . This gives you full kontrol to use, modify, and redistribute it according to your needs.

  • User Friendly: Kontrol gives you the advantage of using languages and testing frameworks you're already familiar with. Kontrol enables developers to write formal specifications as tests in . In addition, this allows developers to reuse their existing test suites for formal verification.

  • Scalable: Kontrol automatically verifies your contracts against your formal specifications via compositional symbolic execution. It generates proofs during the verification process, allowing you to verify contracts of any size. Additionally, Kontrol enhances efficiency by supporting lemmas, loop invariants, and bounded model checking.

  • Trustworthy: Kontrol has a trustworthy mathematical foundation for specifying and verifying smart contracts. It is built on the open-source, validated, and intuitive formal semantics of Ethereum Virtual Machine (EVM) bytecode, . This provides an additional guarantee that the smart contracts you have verified will demonstrate the exact same behavior when executed by the virtual machine.

  • CI Integration: Kontrol seamlessly integrates into continuous integration (CI) pipelines, enabling automated verification with each code commit. Through , it offers cloud-based verification and visualization features, ensuring continuous assurance of smart contract integrity.

Getting Started

Community

To begin using Kontrol, check out our and explore our to see Kontrol in action.

Join our growing community on to connect with other developers, share experiences, and get support.

installation guide
example projects
Discord
Kontrol
BSD-3 Clause License
Foundry
Solidity
KEVM
Kontrol as a Service (KaaS)