Media Kit logo Media Kit

Runtime Verification Inc. is a technology company headquartered in Urbana, Illinois with staff spread across the globe. Urbana, the home of the University of Illinois, and its sister city of Champaign, are located roughly 2.5 hours South of Chicago, 2 hours West of Indianapolis, and 3 hours North of St. Louis. In 2018, Champaign scored the #1 spot in the Best Cities for Recent College Grads ranking, and #2 overall (out of 42 communities) in the Silicon Prairie region. We provide testing and verification services to public and private companies in the embedded and blockchain domains. In the latter we work with infrastructure builders as well as companies building products and providing services supported and/or powered by said infrastructure.

Our mission is accessible trustworthy computing. We accomplish it by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning. K allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.

Our symbol, the two drops (blue and yellow), represent the specification and the implementation. During verification we prove that the two are tightly connected, therefore two rigidity points (RV-Match). For dynamic analysis (RV-Predict and RV-Monitor) some aspects get verified, but not all the implementation, therefore one rigidity point. The two drops mirror each other, but not perfectly.

Runtime Verification symbol

Firefly logo


Firefly is a set of quality assurance tools for Ethereum smart contracts aimed to help developers before the audit and formal verification stages

Download logos

Token verifier logo

ERC20 token verifier

Check your token’s full functional compliance with the ERC20 standard (the approve, transfer and transferFrom functions), before deploying it on mainnet

Download logos

IELE logo


IELE is a virtual machine (VM) for smart contracts, an evolutionary step beyond the Ethereum Virtual Machine (EVM)

Download logos

RV-Match logo


Get to market faster, increase code portability, and save on development and debugging with the most advanced and precise semantics-based bug finding tool.

Download logos

RV-Monitor logo


Automatically check your code for compliance with the Java API, or check custom specifications of your choice.

Download logos

RV-Predict logo


RV-Predict automatically detects the rarest and most difficult data races in your Java and C/C++ code, saving on development and testing effort with the most precise race finder available.

Download logos

company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog