Runtime Verification

Runtime Verification is a formal-methods company, founded in 2010 at the University of Illinois, that combines manual code review with machine-checked verification built on its own K Framework, KEVM and Kontrol tooling. It fits teams that want mathematical properties proven over their contracts or execution environment, not only a manual review. The strongest evidence-backed signal is its public GitHub report index, which held 109 PDF reports spanning 2017 to 2026 when re-counted on 2026-10-14, alongside actively maintained open-source verification tools.

At a glance

Founded	2010, by Grigore Rosu at the University of Illinois at Urbana-Champaign (About)
Headquarters / jurisdiction	Champaign, IL per the GitHub org profile; no address on the contact page
Engagement model	Private firm audit plus formal verification, fuzzing and design review (Contact)
Core specialties	Formal verification (K Framework, KEVM, Kontrol), smart-contract audit, infrastructure/VM review, consensus-protocol verification
Ecosystems / languages	EVM (Solidity), Stellar Soroban (Rust), Algorand, MultiversX, Tezos, Cardano, Solana (Rust), WebAssembly, zkVMs (publications README)
Public report index	github.com/runtimeverification/publications; selected case studies at runtimeverification.com/work
Open-source tooling	K Framework, KEVM (evm-semantics), Kontrol, Komet, Simbolik, mir-semantics and others (GitHub org)
Published pricing	Not published

What they do

The firm's homepage describes three lines of business: software quality assurance (formal verification, fuzzing and property identification for safety-critical systems), "agentic guardrails" for AI agent systems, and data partnerships supplying curated datasets for LLM training. The contact form lists the services a client can request: code audit, formal verification, fuzzing/testing, design review, agentic guardrails, data partnerships and consulting.

Published engagement pages show the process in practice. The Monad engagement was a five-week review combining design review, manual review of code, specifications, formal models and tests, and formal verification using Kontrol, Simbolik and the K Framework. The Espresso Systems engagement ran three weeks (5–19 November 2025) with a walkthrough, manual Solidity review and Kontrol-based property checking; the report was published 24 November 2025.

The About page states 100+ security engagements completed and "25+ senior engineers"; the /work page says "22 Security Experts". The directory's "20+" is a floor consistent with both about page figures.

The firm's recent blog shows work outside blockchain as well: Linux kernel Rust and C verification, medical-device software safety, and AI-assisted fuzzing of the WAMR WebAssembly runtime (September 2026).

Specialties and ecosystem coverage

The publications README groups reports into four categories. A count of the repository tree via the GitHub API on 2026-09-24 found 111 PDFs: 93 under smart contracts, 8 under consensus protocols, 6 under zkVM and 4 under infrastructure. A re-count on 2026-10-14 found 109 PDFs with the repository unchanged since 2026-08-18, so the September total was a miscount; the per-folder split was not redone. A re-count on 2026-10-14 found 109 PDFs with the repository unchanged since 2026-08-18, so the September total was a miscount; the per-folder split was not redone. Some of these are supplemental files belonging to a single engagement, so the number of distinct engagements is lower.

• EVM / Ethereum: Confirmed. Reports include Ethereum Beacon Chain, Casper and Gasper consensus verification, the Ethereum deposit contract, Optimism, Morpho, EigenLayer (design review), Lido Dual Governance (design review), Espresso Systems and Gnosis Safe.
• Stellar / Soroban: Heavily represented in 2024–2026 work (Soroban environment, Soroswap, FxDAO, StellarBroker, Trustless Work, DeFindex and others), plus the Komet verification and fuzzing framework for Soroban.
• Algorand, MultiversX, Tezos, Cardano: Confirmed through multiple reports (Algofi, Tinyman, Folks Finance; Hatom, AshSwap; Quipuswap, Dexter; SundaeSwap, Jpg.Store).
• Solana: Some evidence. The 2025 Kora paymaster-service report is in the infrastructure folder, and the org maintains kompass ("K semantics for Solana") per the org repo listing. The Solana Foundation token-verification case study linked from /work still returned HTTP 404 on 2026-10-14.
• ZK: The zkVM folder includes a zkEVM formal verification report and a Zorp zkVM audit, supporting the directory's "zk-proofs" specialty.
• Not evidenced: No Cosmos, Polygon or Arbitrum-specific reports were found in the index, although those chains appear in the directory entry.

Recent public work

Pulled from the publications README and /work; the README gives years, not exact dates.

1. Moonlight (2026): smart-contract report (index)
2. DeFindex APY Stabilizer (2026)
3. Matrixdock RWA (2026)
4. OctoLend (2026)
5. Monad Execution (published 26 January 2026): 0 critical/high, 4 medium and 10 low/informative findings (engagement page)
6. Espresso Systems staking contracts (November 2025): 1 critical/high, 0 medium and 12 low/informative findings (engagement page)
7. Kora paymaster service (2025, Solana)
8. Zivoe Vault (2025, formal verification report)
9. Octant v2 (2025)
10. Token Wrap, TokenOps, EquitX, Trustless Work, Levery, StellarBroker, ClickPesa, FxHash (2025)

Research, tooling and methodology

• K Framework: A rewrite-based semantic framework for formally defining programming languages and virtual machines, released in 2014 per the About page. It is among the most-starred repos in the GitHub org.
• KEVM (evm-semantics): Formal semantics of the EVM in K, dated 2017 on the About page.
• Kontrol: Combines KEVM and Foundry so developers can run symbolic execution over existing Foundry tests; BSD-3-Clause (repo).
• Komet: Formal verification and fuzzing for Soroban contracts (repo).
• Others: The org repo listing also shows mir-semantics (Rust MIR), skribe (property testing for Arbitrum Stylus contracts), simbolik-vscode (a Solidity debugger) and ercx-tests (property tests for token standards). The core repos were pushed to in September 2026.
• Methodology in reports: Engagement pages report findings in Critical/High, Medium and Low/Informative bands (Monad). No standalone methodology document was found.
• Credentials: The founder's matching-logic work (2019) is cited on the About page. The /work page references three NASA SBIR grants.

Track record and incidents

• Cork Protocol (28 May 2025, about $12M): rekt.news reports that the exploit used the CorkHook contract's beforeSwap function. It quotes Runtime Verification as saying that verification of hook functions was out of scope due to time constraints, and states that the vulnerable CorkHook contract was outside the defined scope of Runtime Verification, Sherlock and Quantstamp. Runtime Verification's Cork formal-verification summary (2024) is in its publications index. On this reporting, the exploited code was not in the scope the firm verified. Cork's own post-mortem returned HTTP 403 and could not be read in this pass.

No other reputable post-audit incident naming the firm was found in this pass.

Who should consider them, and who might look elsewhere

• Good fit: Teams that want formal verification of invariants on EVM contracts, especially teams already using Foundry, since Kontrol reuses Foundry tests. Also teams building on Stellar Soroban, Algorand or MultiversX, where the public report history is deep, and teams building L1 or VM infrastructure (Monad, Wasmi, Soroban environment) or consensus protocols.
• Might look elsewhere: Teams needing a fast, low-cost manual review only. The firm's public work centres on verification-heavy engagements, and its own Cork scope statement shows that time-boxing can leave components unverified. Teams focused on Cosmos, Polygon or Arbitrum-native codebases will find little public evidence in the index. Recent blog output also shows the firm spreading into AI guardrails, Linux and medical-device work, so confirm staffing for blockchain engagements when scoping.
• Scope advice: Whichever firm you hire, list every contract that will hold or route value, including hooks and integrations, and ask what formal properties will and will not be covered.

How to engage

Use the multi-step Work With Us / contact form. It asks for the project name, website, services of interest, timeline (ASAP, 2–4 weeks, or 1–3 months), and a project description. The firm says its team will follow up to scope the engagement. Before you submit, have ready: the repo and commit, the contracts in scope, specifications or invariants you want proven, the existing test suite (Foundry tests help with Kontrol), and your deadline.

Gaps and unverified claims

• The Solana Foundation case study linked from /work returns HTTP 404, so the Solana Foundation engagement listed in the directory could not be confirmed from a report.
• Cosmos, Polygon and Arbitrum are listed as chains in the directory but are not evidenced in the public report index.
• The directory's "20+" team size is a floor; the about page says 25+ senior engineers and /work says 22 security experts. Engagement count (100+) is self-reported on the About page.
• Pricing and typical turnaround are not published. The directory's 8–16 week turnaround could not be verified; published engagements ran three to five weeks.
• Cork Protocol's own post-mortem could not be loaded (HTTP 403).
• The X/Twitter handle listed in the directory was not verified in this pass.

Sources

1. Runtime Verification homepage, accessed 2026-09-24
2. Runtime Verification /work, accessed 2026-09-24
3. Runtime Verification About, accessed 2026-09-24
4. Runtime Verification Contact / Work With Us, accessed 2026-09-24
5. Monad public report page, accessed 2026-09-24
6. Espresso Systems public report page, accessed 2026-09-24
7. Publications repository, accessed 2026-09-24
8. Publications README (raw), accessed 2026-09-24
9. Publications repository tree (GitHub API, used for PDF count), accessed 2026-09-24
10. Runtime Verification GitHub org, accessed 2026-09-24
11. GitHub org repository listing (API), accessed 2026-09-24
12. Kontrol repository, accessed 2026-09-24
13. Komet repository, accessed 2026-09-24
14. Runtime Verification blog, accessed 2026-09-24
15. rekt.news: Cork Protocol, accessed 2026-09-24