Skip to main content
Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

View on GitHub (opens in a new tab)K Semantics of the Ethereum Virtual Machine (EVM) on X (opens in a new tab)

See next

hax

About 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.

Tags

  • Security
  • Education
  • Analytics
  • Formal verification
  • Symbolic execution
  • Debugging tools
  • Runtime verification
  • Vyper

Repositoryruntimeverification

Info

Type
Formal verification
GitHub stars
595

Similar tools

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.

Kontrol - formal verification tool based on Foundry and KEVM

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.

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.