Blockchain Advisory Services

“Building on the blockchain” — be it smart contracts, tokens, protocols, or virtual machines — is challenging. We’ve been there. Now we’d like to share our experiences and offer our expertise via an advisory service we call “RV office hours”. During your office hours you will receive targeted advice from an RV senior engineer on the verification topic of your choice. Look at it as an affordable way to reduce existing tech debt and frustration or prevent its accumulation from the beginning.

You can book blocks of office hours on any of the following topics:

Smart Contracts — There are things you should know before you have your contract audited or formally verified. In fact, there are details you should know even before you write your smart contract. Feel free to read more about our approach. You can also check out our public reports and the collected list of known smart contract vulnerabilities.

Consensus Protocols — Our approach to protocol verification is centered around formal methods. First, we build formal specifications of the protocol’s design and its properties. Second, we mathematically verify that protocol’s design meets its expected requirements. We developed formal models of Casper 1 | 2 | 3 and Algorand 1 | 2 | 3 | 4.

Virtual Machines — In partnership with blockchain research firm, IOHK, we designed and developed IELE, a new virtual machine that represents an evolution of sorts of the Ethereum virtual machine (EVM). It leverages the KEVM project, which successfully demonstrated that a K formal specification can automatically generate a "fast enough" VM.

Tokens — For the Ethereum ecosystem we specified ERC20-K and ERC777-K, the mathematically rigorous formalization of the ERC20 and ERC777 token standards. These formalizations facilitate formal verification of token implementations.

Formalized Languages — Developing formal analysis tools for a programming language takes a substantial amount of work. The K Framework consists of several language-independent program analysis tools automatically derived from a formal definition of the target language’s syntax and semantics. If you need help formalizing your language in K, take a look at a few examples that have been successfully formalized: C, Java, JavaScript, PHP, Python, EVM, IELE.

Let's Get Started

Let us know what package works best for you at .









Our top team of experts