K framework and KEVM: Executable semantics for the EVM and zkVM equivalence work
================================================================================

K 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-harness, Lean backend for K
Approach: Rewriting-based semantics from which interpreters, symbolic executors and provers are derived
Access: Open source
Status: Active, mature
Strengths: Executable and provable from one definition. | KEVM is battle tested. | Lean backend bridges to the ZK ecosystem.
Limits: Specialist tooling. | Not a circuit verifier. | Heavy for small projects.
Firms using it: Runtime Verification
Sources: https://kframework.org | https://github.com/Verified-zkEVM/Overview

Source page: https://sorryfree.com/frameworks/k-framework/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13