Blockchain Advisory Services logoBlockchain 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.

Alchemix
Algorand
Bihu
Casper protocol
Cosmos
Cryptape blockchain
Dapper Labs
Element Finance
Emurgo
Ethereum
Ethereum Community Fund
Ethereum Enterprise Alliance
Ethereum Trust Alliance
Gnosis
IOHK
Maker
MultiversX
Panvala
Parity
PlatON
Polkadot
Stakefish
StakerDAO
StakeWise
Tezos
Tinyman
Uniswap
Web3 Foundation
Whiteblock

Contact us if you need advice before starting with any type of blockchain project:

Smart Contracts
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
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
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
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
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.

Blockchain advisory team members