Skip to main content
Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

View on GitHub (opens in a new tab)Kontrol - formal verification tool based on Foundry and KEVM on X (opens in a new tab)

See next

Act

About Kontrol - formal verification tool based on Foundry and KEVM

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.

Tags

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

Repositoriesruntimeverification

Info

Type
Formal verification
GitHub stars
126

Similar tools

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

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

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.