Kontrol

Open Source

Formal verification tool that combines KEVM with Foundry, letting developers verify smart contracts symbolically using existing test suites without learning new languages.

About

Kontrol, built by Runtime Verification, symbolically executes existing Foundry tests using the K Framework's formal EVM semantics (KEVM). Unlike testing which samples inputs, Kontrol proves properties hold for all possible states. Open-source under BSD-3 license, it bridges the gap between practical testing and formal verification by reusing developers' existing Foundry tests as verification specifications.

Categories

Formal Verification Testing

Chains

ethereum polygon arbitrum optimism

Install

kup install kontrol

Related Tools

Foundry Fuzz

Pairs with Kontrol

Certora Prover

Pairs with Kontrol

Halmos

Pairs with Kontrol

Quick Info

Pricing
free
Open Source
Yes
Last Updated
2026-04-05

Links

Website GitHub Documentation