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

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

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

IELE logo

IELE

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

Explore IELE

Testimonials





Newsletter





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