Runtime Verification Inc.

What We Offer

Smart contract verification

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

Choose your options

Protocol verification

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

Understand the process

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

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 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

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

Explore IELE

Testimonials

Now we are happy to announce the completion of an extra layer of security: "formal verification". It was a huge effort by @rv_inc and done with support from @ethereumecf. Gnosis will soon start moving funds to this verified version of the contract.

Martin Köppelmann @koeppelmann

I'm excited to be working with Runtime Verification @rv_inc again. We just signed a seven figure deal to restart work on IELE. Welcome back K, we missed you.

Charles Hoskinson @IOHK_Charles

$EGLD gets formal verification tools from @rv_inc With otherwise expensive & complex testing tools available in the Elrond devkit the overall security of our DeFi ecosystem raises to meet institutional-grade requirements.

Elrond eGold @ElrondNetwork

The work been done by @rv_inc, it’s incredible. I only have good things to say and the more I learn about K-Framework, the more ideas I get to bring even more innovation to @Cardano 💪 #cardano

Nico Arqueros @NicoArqueros

The first ever ERC20 formal verification spec was done by @rv_inc they now made one for ERC777 as well! The next token standard. Now we need automated gen. proofs and checkers to run those!

Fabian Vogelsteller @feindura

@ercwl @rv_inc Yeah, the KEVM is amazing. We also built https://github.com/dapphub/klab to be able to explore the complete space of execution paths for an ethereum contract. Browser version in the pipeline!

Martin Lundfall @MartinLundfall

This report on @rv_inc's verification of RANDAO's possible randomness bias under worst-case adversarial conditions using statistical model checking is one of the most underrated new papers in cryptocurrency security/modeling, IMO.
rdao-analysis.pdf

Philip Daian @phildaian

To make the Gnosis Safe one of the most secure multisigs on the market, we worked with formal verification pros @rv_inc and updated our smart contracts. Check out the full report here 👉
GnosisSafe_RuntimeVerification.pdf

Gnosis Safe @gnosisSafe

Another major achievement is the Meta VM Elrond brings by building a GO backend to K framework. Through this we will support 3 VMs at the same time for max flexibility: EVM, WASM, IELE + formal verification

Beniamin Mincu ⚡ @beniaminmincu

Warming up to proposing the Jello Paper as the canonical EVM spec, and would love everyone's thoughts. IMO the Jello Paper way clearer and complete versus the current Yellow Paper. Kudos to the KEVM folks 🎉 https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389

Brooklyn Zelenka 🏳️‍🌈 @expede

Just released v0.11.3 with critical bug fix to the eth2 state transition spec. Special thanks to @daejunpark for finding the bug while doing formal verification on the eth2 spec for @rv_inc! https://github.com/ethereum/eth2.0-specs/releases/tag/v0.11.3

Danny Ryan @dannyryan

@rv_inc! completes the formal verification of the eth2 deposit contract bytecode! https://github.com/runtimeverification/verified-smart-contracts/blob/master/deposit/bytecode-verification/deposit-spec.ini

Danny Ryan @dannyryan