# Kontrol

<div data-full-width="true"><figure><img src="/files/FTLPMjiPL5eTntFngXRv" alt=""><figcaption></figcaption></figure></div>

[**Kontrol**](https://github.com/runtimeverification/kontrol) 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 [BSD-3 Clause License](https://github.com/runtimeverification/kontrol/blob/master/LICENSE). 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 [Foundry](https://book.getfoundry.sh/) tests in [Solidity](https://soliditylang.org). 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, [KEVM](https://github.com/runtimeverification/evm-semantics). 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 [Kontrol as a Service (KaaS)](https://docs.runtimeverification.com/kaas), it offers cloud-based verification and visualization features, ensuring continuous assurance of smart contract integrity.

### Getting Started

To begin using Kontrol, check out our [installation guide](/kontrol/overview/readme/installations.md) and explore our [example projects](/kontrol/guides/kontrol-example.md) to see Kontrol in action.

#### Explore the Codebase with AI

If you want to dive deeper into Kontrol's architecture and implementation, check out [**Kontrol on DeepWiki**](https://deepwiki.com/runtimeverification/kontrol)—an AI-powered interactive documentation that lets you ask questions about the codebase.

### Community

Join our growing community on [Discord](https://discord.gg/CurfmXNtbN) to connect with other developers, share experiences, and get support.


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/kontrol/overview/readme.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.