“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.
Contact us if you need advice before starting with any type of blockchain project:
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 verificationis 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.
