Runtime Verification website hero image Runtime Verification website hero image

We love formal methods

We specify, model and verify code and designs using formal logic.
Properties can be anything you can specify in logic. It can range over a function, or an entire program.
We check those properties against concrete inputs (runtime verification) and symbolic inputs (formal verification), and explore all possible behaviors of the code, to give you the highest possible assurance.

Our approach is based on the K Semantic Framework.

What We Offer

Smart Contract verification icon

Smart contract verification

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

Choose your options

NFT Checker logo

NFT Checker

Mints can be gamed, tokens can be stolen, gas can be wasted, and bad code makes people wary of rug pulls.

Let us help

Protocol Verification icon

Protocol verification

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

Understand the process

Blockchain Advisory Services icon

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!

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

Give it a try

ERC20 icon

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


Blog Posts

All Blog Posts

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