Take Kontrol of Your Smart Contracts

Combine KEVM and Foundry to verify properties in Solidity smart contracts


Key Features

Supports Solidity Test Development
No need to learn new tools or write tests in a proprietary language.
Complete EVM Semantics Foundation
Based on the most complete EVM, including gas, storage, transaction modeling, and RLP encoding.
Seamless Foundry Integration
Leverage Foundry tests and cheatcodes without having to rewrite them for FV testing.
Advanced Feature Support
Including lemmas, loop invariants, and bounded model checking to facilitate the reasoning process.
Advanced Visualization
Expedites debugging and identification of code vulnerabilities.

Why Kontrol?

Formal Verification = Better Security
Formal methods ensure code correctness before contracts go live on mainnet.
Easy Integration into CI Automation Processes
Leveraging K as a Service (KaaS), code changes are validated as they happen.
New Features Actively Under Development
Kontrol is constantly evolving to keep pace with the ever-changing web3 market.
Fully Supported by Runtime Verification
We are here to answer questions about Kontrol and to help resolve issues with your code.
Open Source
Kontrol is fully open-source, so you can use it freely in your project.
Easy to Use and Integrate
Kontrol leverages Foundry tests as specification, providing an easy entry to formal verification.

Meet our friends and collaborators

We work with strong teams and advanced companies providing the best possible service to all.

Ethereum Foundation
Gnosis Chain

Read our blog posts


Get in touch

If you want to learn more about how Kontrol can help secure your Project, please complete the form below and we will contact you: