background

Take Kontrol of Smart Contracts

Formal Verification made simple, so you don't have to settle for fuzzing.

why kontrol

Easy to use, powerful Formal Verification

Free to use, open-source public good
We believe in open-source software. Run proofs on your local machine, reach out to us for support.
Uses existing Foundry tests directly
Install Kontrol, build your project, start symblically executing existing Foundry tests in minutes.
Formal Verification = Better Security
Formal methods give the highest code assurances for smart contracts. Symbolic execution is like fuzzing for the entire input space.
Use Solidity to write proofs
No need to learn new tools or write tests in a prioprietary language.
Kontrol line break
how it works

As Simple as Using Foundry

kontrol_rocks@formal_verification: ~
install_kontrol:~$ kup install kontrol

build_your_app:~$ cd your_app
build_your_app:~$ kontrol build

prove_a_test:~$ kontrol prove --match-test CounterTest.testSetNumber

see_results:~$ kontrol list
foundry_build_by_friends@paradigm: ~
install_foundry:~$ curl -L https://foundry.paradigm.xyz | bash

build_your_app:~$ cd your_app
build_your_app:~$ forge build

run_a_test:~$ forge test --match-test CounterTest.testSetNumber

Kontrol line break
partners

Trusted by the Best to Secure Billions of TVL

Lido
Optimism
Ethereum Foundation
Gnosis Chain
Paradigm
Runtime Verification
Kontrol line break
learn more

Built by Seasoned Formal Verification Experts

Easy Integration into CI Automation Processes
Option to Outsource the Compute using KaaS
Complete EVM Semantics Foundation
Based on the most complete EVM, including gas, storage, transaction modeling, and RLP encoding.
Advanced Feature Support
Including lemmas, loop invariants, and bounded model checking to facilitate the reasoning process.
Kontrol line break
contact us

Get in Touch with Runtime Verification