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 tool for helping Ethereum smart contract developers visualize and discover holes in the existing test-set, and guide them towards full coverage of their contract.

Try it now

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

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