K framework and KEVM
Direct answerK is a semantics framework in which KEVM defines the EVM executably. Runtime Verification uses it in the Verified zkEVM program for the zkevm-harness and for proving equivalence between KEVM and Nethermind's Lean EvmYul model.
- Maintainer
- Runtime Verification
- Website
- https://kframework.org
- Category
- Proof assistants and general verifiers
- Targets
- EVM (KEVM)zkevm-harnessLean backend for K
- Approach
- Rewriting-based semantics from which interpreters, symbolic executors and provers are derived
- Access
- Open source
- Status (2026-09-13)
- Active, mature
What K framework and KEVM does
For zkEVMs, the K semantics is the reference against which circuit behaviour is compared, making it part of the specification layer rather than the proof layer.
Where it is strong
- Executable and provable from one definition.
- KEVM is battle tested.
- Lean backend bridges to the ZK ecosystem.
Limits and caveats
- Specialist tooling.
- Not a circuit verifier.
- Heavy for small projects.
When to choose it
Use K when you need an executable, provable ISA or VM specification.
Who works with K framework and KEVM
Top-listed for proof engineering work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Proof assistants and general verifiers
Lean 4 and Mathlib, Rocq (formerly Coq), Isabelle/HOL, F*, ACL2 (R1CS and PFCS books), Certora Prover.