Skip to main content
Kontrol - formal verification tool based on Foundry and KEVM
Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

Foundry · Education · Governance · Formal verification · Solidity · Runtime verification · Contract deployment · Static analysis

Social (opens in a new tab)runtimeverification/kontrol(118 ☆) (opens in a new tab)runtimeverification/optimism-ci(4 ☆) (opens in a new tab)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆) (opens in a new tab)runtimeverification/yearn-v3-term-vault(0 ☆) (opens in a new tab)runtimeverification/Depeg-swap(0 ☆) (opens in a new tab)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆) (opens in a new tab)

Kontrol lifts Foundry property tests into KEVM-backed proofs so you can chase formal guarantees with less hand-written specification work than raw KEVM alone.

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM is the K-framework executable semantics of the EVM: point it at bytecode when you need conformance-checked execution, symbolic exploration, gas reasoning, or proofs that track Ethereum's rules closely.

hax

hax is a tool for high assurance translations of a large subset of Rust into formal languages such as F* or Rocq.

Act

Act

Act is Ethereum's declarative specification language and toolchain for describing all behaviors of an EVM program so SMT solvers, theorem provers, or economic analysis tools can reason about bytecode-level correctness and incentive compatibility, including automatic refinement proofs against concrete implementations.

Verifereum

Verifereum

Verifereum connects Ethereum smart contracts to HOL4-backed theorem proving so you can aim at very strong correctness claims when automated SMT approaches are not enough.