Cowrie Research

runtime-verification-primary-sources-2026-04-30

3 min read

Runtime Verification primary sources — 2026-04-30

Project status in this pass

  • No canonical standalone whitepaper or litepaper surfaced.
  • The clearest current source of truth is the company site, GitHub organization, public publications repo, and the first-party docs/readmes for Kontrol and KEVM.

Primary-source snapshots

1) Official homepage

  • URL: https://runtimeverification.com/
  • Key excerpt:
    • The homepage frames Runtime Verification as “Software Assurance for the AI Age” and says it provides “High-assurance cybersecurity consulting for critical systems.”
    • It says the team is “Rooted in formal methods” and works closely with organizations building software “that cannot fail.”
    • The visible page also links directly into blockchain-relevant public materials such as audit blog posts and public reports.

2) GitHub organization

  • URL: https://github.com/runtimeverification
  • Key excerpt:
    • The org description says Runtime Verification specializes in formal verification of software systems and aims to provide open-source formal verification and developer tooling.
    • It explicitly says the mission is to reduce audit costs and enable “continuous formal verification and testing on each commit.”
    • The org highlights active projects including K Framework, Kontrol, Simbolik, KEVM, KWasm, and KMIR.

3) Publications repository

  • URL: https://github.com/runtimeverification/publications
  • Key excerpt:
    • The public repository organizes first-party outputs into consensus-protocol formal verification, infrastructure audit/fuzzing/formal verification, and smart-contract security audit/formal verification.
    • Visible entries include Ethereum Gasper, Ethereum Beacon Chain, Algorand, EigenLayer, Morpho, Gnosis Safe, Uniswap, Espresso Systems, Monad, and many other named engagements.
    • This repo is the strongest single artifact for understanding the breadth and continuity of Runtime Verification’s blockchain-facing work.

4) Publications README

  • URL: https://raw.githubusercontent.com/runtimeverification/publications/master/README.md
  • Key excerpt:
    • The README exposes a long categorized index of reports and linked artifacts rather than a thin marketing-only portfolio.
    • The category split matters because it shows Runtime Verification spanning protocol verification, infrastructure review, and smart-contract work instead of operating only as an EVM audit shop.

5) Kontrol docs

  • URL: https://docs.runtimeverification.com/kontrol
  • Key excerpt:
    • Kontrol is described as a formal verification tool for EVM smart contracts that integrates with Foundry so developers can use Solidity tests as formal specifications.
    • The docs emphasize accessibility for non-specialists, compositional symbolic execution, CI integration, and the KaaS hosted verification surface.
    • The page also says Kontrol is built on KEVM, reinforcing that Runtime Verification maintains its own foundational verification stack.

6) Kontrol repository README

7) KEVM repository README

  • URL: https://raw.githubusercontent.com/kframework/evm-semantics/master/README.md
  • Key excerpt:
    • The KEVM repo says it provides a model and formal semantics of the EVM in K.
    • The repository structure section shows detailed semantic components such as execution rules, gas, schedules, ABI handling, hashed locations, and symbolic-execution helpers.
    • This is strong evidence that Runtime Verification’s public surface includes foundational EVM-verification infrastructure, not just services.

Working conclusion

Runtime Verification is best cataloged as formal-verification security and verification-tooling infrastructure with a particularly deep crypto footprint. The combination of a public reports archive, foundational semantics projects, and developer-facing verification tooling makes it materially broader than a conventional audit firm.

Graph View