Runtime Verification

• Name: Runtime Verification
• URL: https://runtimeverification.com/
• Category: formal-verification company / software-assurance workflow operator / proof-tooling steward
• Tags: ethereum-ecosystem
• Summary: Runtime Verification belongs in companies/, not projects/, because the useful question is not just what verifier exists? but which named operator stewards Kontrol, KEVM, the broader K-based verification stack, public report publication, and the managed workflow that teams may start treating as release-gating truth? The practical leverage sits less in any one proof artifact than in who chooses the modeling surface, maintains the semantics and toolchain, publishes the examples and reports other teams copy, and packages formal verification into customer engineering workflow.
• What it does:
  • Performs formal verification, design review, fuzzing, and audit work for smart contracts, blockchain infrastructure, and other critical software systems
  • Maintains reusable verification tooling including Kontrol for EVM smart contracts, KEVM for executable EVM semantics, and broader K Framework-based infrastructure
  • Publishes a large first-party publications repository spanning consensus protocols, infrastructure systems, smart-contract work, white papers, and related research outputs
  • Positions Kontrol as a way for Solidity and Foundry users to turn existing tests into formal specifications instead of adopting a wholly separate workflow
  • Supports CI-oriented and hosted verification workflow, including the Kontrol-as-a-Service / KaaS surface referenced in official materials
  • Operates across crypto and adjacent critical-software domains, but its public client and report footprint shows especially strong depth in Ethereum, EVM protocols, staking, and blockchain consensus systems
• 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 tooling that reduces audit costs and enables continuous formal verification and testing on each commit
  • The public publications repository organizes official output across academic papers, white papers, infrastructure work, and smart-contract reviews, which is a strong signal that Runtime Verification is operating a durable methodology-and-publication surface rather than only running private consulting engagements
  • The Kontrol docs describe 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 makes the maintained semantics layer itself part of the company-controlled surface rather than a disposable implementation detail
  • Taken together, the current primary-source corpus suggests Runtime Verification should be cataloged as verification-and-assurance infrastructure under a named company boundary, not as a standalone protocol or product page
• Whitepaper: No canonical Runtime Verification company 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.
• Sources:
  • https://runtimeverification.com/
  • https://github.com/runtimeverification
  • https://github.com/runtimeverification/publications
  • https://raw.githubusercontent.com/runtimeverification/publications/master/README.md
  • https://docs.runtimeverification.com/kontrol
  • https://raw.githubusercontent.com/runtimeverification/kontrol/master/README.md
  • https://raw.githubusercontent.com/kframework/evm-semantics/master/README.md

Internal linkages

• Project-layer alias: runtime-verification.
• Useful adjacent company reads: certora, trail-of-bits, and informal-systems.
• Useful tooling-centered contrast where the question stays closer to reusable product surface than one operator shell: certora.

Protocol / company boundary

• There is no especially clean standalone Runtime Verification protocol boundary doing the analytical work here.
• The meaningful surface is the company-run mix of formal-semantics maintenance, proof tooling, public methodology, published reports, and managed verification workflow that sits around other teams’ build and release processes.
• That is why Runtime Verification belongs in companies/: the sharper questions are about who stewards the semantics, examples, proof workflow, and assurance posture other teams inherit, not about one isolated artifact.

Control surface

• Practical leverage sits in which properties get modeled, which assumptions stay outside the proof boundary, how semantics and examples evolve, which ecosystems receive first-class support, and how much downstream engineering workflow starts depending on Runtime Verification-maintained tooling or review outputs.

• The company does not directly control the protected protocols, but it can materially shape how teams specify correctness, what they bother to prove, and which verification patterns become normal before deployment.

• Read Runtime Verification as a formal-verification company and workflow steward first, not as a neutral protocol primitive.

• Last reviewed: 2026-08-09 UTC