Runtime Verification

Direct answerRuntime Verification maintains the K framework and KEVM and, within the Verified zkEVM program, the zkevm-harness and the equivalence proof between KEVM and Nethermind's Lean EvmYul model. It audits and verifies smart contracts and VM implementations.

Website: https://runtimeverification.com
Headquarters: Urbana, Illinois, United States
Focus: K framework, KEVM, zkevm-harness, EVM equivalence with Lean models
Index position: #8 of 11
Founded: 2010

Services

Executable semantics and equivalence proofs for VMs
Smart-contract formal verification with K
zkEVM harness and conformance work

Frameworks this firm builds or uses

K framework and KEVM.

Public evidence

Best fit

Choose Runtime Verification when the specification layer (an ISA or VM semantics) is what needs to be executable and provable.

Other firms on this index

zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Certora, Trail of Bits, Symbolic Software

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt