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