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.
how it works
As Simple as Using Foundry
1Install Kontrol
2 Build the Project
3 Prove a Test
4 See the Results
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
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
build_your_app:~$ cd your_app
build_your_app:~$ forge build
run_a_test:~$ forge test --match-test CounterTest.testSetNumber
partners
Trusted by the Best to Secure Billions of TVL
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.
contact us