Turn complexity into confidence
Runtime Verification designs formal models for high-value application domains, then uses the models to develop domain-specific products and services focused on correctness and security.


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

Try it now

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

Check your token

Blockchain Advisory Services

Receive targeted advice from an RV senior engineer on the verification topic of your choice: smart contracts, tokens, protocols, or virtual machines

Hire us!

Smart Contract Verification

Prove the correctness of smart contracts compiled for the Ethereum and Cardano virtual machines

Prove your contracts

Protocol Verification

Increase confidence in the correctness and security of the decentralized system powered by your protocol

Prove correctness


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

Explore IELE

Supporters & Contributors

Let's Get Started

Interested in RV’s formal verification services? Please complete the form below. Or send your questions to .

The K Formal Semantics Framework

K lets you design the formal semantics of your programming language in a modular and intuitive way, then uses the semantics to generate a suite of language tools including a parser, execution engine, symbolic execution engine, state-space explorer, and even a program verifier.

Read more

The K Community

The K Team was started in 2003. K has been continuously developed since then, with the center of the community being the FSL research group at the University of Illinois in Urbana-Champaign, USA.

Visit the community