Blockchain advisory

RV office hours: targeted advice from a senior engineer

Building on a blockchain, whether it is smart contracts, tokens, protocols or virtual machines, is hard. We have been there. Book time with an RV senior engineer on the verification topic of your choice: an affordable way to clear existing tech debt, or to avoid accumulating it.

Teams we have advised

What people ask about

Smart contracts

There are things worth knowing before a contract is audited or formally verified, and things worth knowing before it is written at all. Read about our approach, or go straight to the public reports and the collected list of known smart contract vulnerabilities.

Consensus protocols

Our approach to protocol verification is centred on formal methods: build a formal specification of the design and its properties, then prove mathematically that the design meets its requirements. We did this for Casper (1, 2, 3) and for Algorand (1, 2, 3, 4).

Virtual machines

With the blockchain research firm IOHK we designed and built IELE, a virtual machine that evolved out of the EVM. It builds on KEVM, which demonstrated that a K formal specification can generate a VM fast enough to actually run.

Tokens

For the Ethereum ecosystem we specified ERC20-K and ERC777-K, mathematically rigorous formalizations of the ERC20 and ERC777 standards. They are what makes formal verification of a token implementation tractable.

Formalized languages

Building formal analysis tools for a language is a large piece of work. The K Framework derives a set of language-independent program analysis tools automatically from a formal definition of the target language's syntax and semantics. If you need help formalizing your language in K, these have been through it already: C, Java, JavaScript, PHP, Python, EVM and IELE.

Who you would be talking to

Need advice before you start building?

Book office hours