Cowrie Research

runtime-verification

3 min read

Runtime Verification

  • Name: Runtime Verification
  • URL: https://runtimeverification.com/
  • Category: formal-verification security / smart-contract verification tooling / blockchain protocol audit and research infrastructure
  • Summary: Runtime Verification is one of the stronger proof-heavy security shops in the corpus. The note matters because the firm is not just selling reports; it also ships reusable verification infrastructure like Kontrol and KEVM.
  • What it does:
    • Performs formal verification, design review, fuzzing, and audit work for smart contracts, blockchain infrastructure, and other critical software systems
    • Maintains a large first-party publications repository with public reports spanning consensus protocols, infrastructure systems, and smart-contract engagements
    • Ships open-source verification tooling including Kontrol for EVM smart contracts, KEVM for executable EVM semantics, and broader K Framework-based infrastructure
    • Positions Kontrol as a way for Solidity and Foundry users to turn existing test suites into formal specifications rather than adopting an entirely separate workflow
    • Supports continuous-verification-style workflows through CI integration and a hosted Kontrol-as-a-Service / KaaS surface referenced in the docs
    • Operates across crypto and adjacent critical-software domains, but its public client/report history shows especially strong depth in Ethereum, EVM protocols, staking, and blockchain consensus work
  • Key claims:
    • The official homepage says Runtime Verification provides “Software Assurance for the AI Age,” is “Rooted in formal methods,” and works with teams building “software that cannot fail”
    • The GitHub organization says the company specializes in formal verification of software systems and aims to deliver open-source formal verification and developer tooling that reduce audit costs and enable “continuous formal verification and testing on each commit”
    • The public publications repository organizes first-party reports across consensus protocols, infrastructure, and smart contracts, including named work on Ethereum consensus research, EigenLayer, Morpho, Espresso Systems, Uniswap, Gnosis Safe, and many others
    • The Kontrol docs describe the tool as an open-source formal-verification system for EVM smart contracts that integrates with Foundry, reuses Solidity tests as specifications, supports CI workflows, and is built on KEVM
    • The KEVM repository describes KEVM as a model and formal semantics of the EVM in K, which is a strong signal that Runtime Verification is not only reviewing contracts but also maintaining foundational verification infrastructure
    • Taken together, the current primary-source corpus suggests Runtime Verification should be cataloged as verification-and-security infrastructure rather than as a simple audit boutique
  • Whitepaper: No canonical Runtime Verification whitepaper or litepaper surfaced in this pass. The strongest current sources of truth are the official site, GitHub organization, public publications repository, Kontrol docs, and KEVM/Kontrol repositories; see ../whitepapers/runtime-verification-primary-sources-2026-04-30.md.

Internal linkages

Control surface

Graph View

Backlinks