Team logoSmart Contract Analysis and Verification

We have experience in formal modeling, analysis, safety, security, validation and verification, having pioneered many of the techniques used by the community, such as the K-framework and language-independent verification technology. We've worked with NASA, DARPA, Boeing, and Toyota, on formalizing and verifying safety and mission critical systems, and with IOHK and the Ethereum Foundation to formally model and verify not only smart contracts, but also consensus protocols, programming languages and virtual machines.

Interested in reviewing the work we’ve done to date? Please visit our GitHub repository, or click on one of the links below.


Analysis and verification packages

We believe our primary competitive advantage, and thus main point of differentiation as compared to competing security service providers, is our proven expertise in formal verification and assurance.

Test coverage

Design Review

Runtime Verifications’s speciality in formal methods allows us to take a critical look at your product’s design. Errors in design are the most critical and the most costly to fix, so it’s best to catch and correct them early. Our experienced engineers will review your specifications and implementation, consulting continuously with your developers, to understand your product, ensure there are no holes or inconsistencies in your design, and discover important properties and invariants for the product’s safe operation. We will contribute directly to your specifications where issues are found, which can be used as part of the public documentation of the product and lays the foundation for later steps in a security audit.


Contact us

Symbolic bytecode analysis

Code Review

Following Design Review, our team will have a thorough understanding of your product and a completed specification to work from as reference. We systematically review your codebase, ensuring that it conforms to the specifications produced in the Design Review phase. Our training in formal methods allows us to take a verification oriented approach to this review by manually proving the important properties of the product hold for each component of the code. All issues found in the process will be documented and reported to your developers in real-time.


Contact us

Traditional security audit

Security Audit Report

Following Design Review and one of either Code Review or Formal Verification, we can produce a unified report describing the work we’ve done with your product. This report can be published among our public audit reports as a record of this work. The report will include any design documentation we have produced, important properties we have specified, a description of the scope of the audit, any issues we discovered over the entire course of the engagement, and any verification artifacts that are relevant for the codebase.


Contact us

Formal modeling

Formal modeling

This package applies to any system, including programming languages, virtual machines and protocols, not only to smart contracts. For smart contracts, it includes the following:

  • Formally specify the contract’s business logic to produce a formal model that provides a precise, unambiguous, and comprehensive documentation. The model is executable, so it can serve as a reference implementation, and is used to generate and support “blackbox testing”.

  • Validate the critically important properties of the contract’s business logic to provide the ultimate formal guarantee for the absence of loopholes. Please note this package does not include formal verification of the smart contract code.


Contact us

Formal Verification

Formal Verification

The highest level of guarantee that can be achieved for a codebase is formal verification, where we prove that the code will always behave as expected. In this process, we translate the discovered properties and specifications from the Design Review phase into machine-readable specifications via our property-testing framework. In the case of Ethereum, we use Kontrol, which enables writing verification conditions as Solidity property tests. This intuitive approach to verification allows us to directly enable the verification in your CI process and enables your developers to maintain and continue the verification work past the engagement’s end.


Contact us

How smart contract analysis and formal verification work

Our team will meticulously review your code line by line checking for bugs, errors, security vulnerabilities, and exploits. On top of this manual review, we incorporate our own bounded model checking tool, powered by the K-framework using its symbolic execution capability, to augment and enhance your review.

Meet and greet

Meet & greet

  • You present your company, dive into your contract, and identify requirements.

  • RV runs through available review and verification packages.

  • RV introduces a typical engagement from start to finish.

Package selection

Package Selection & Agreement

  • You select the package that best meets your needs.

  • RV provides an estimated timeline for delivery of your engagement.

  • We sign contract and you provide initial deposit.

Report

Engagement & Report

  • RV reviews and/or verifies your code.

  • RV drafts preliminary report and provides debrief on findings.

  • You implement code improvements.

  • RV delivers and publishes final report (requires client approval).

Alchemix
Algodex
Algorand
AshSwap
Atlendis
Band Protocol
Blockswap
Casper protocol
Cosmos
Cryptape blockchain
Dapper Labs
Dexter
Element Finance
Emurgo
Ethereum
Ethereum Community Fund
Ethereum Enterprise Alliance
Ethereum Trust Alliance
EXA Finance
Folks Finance
Galactic
Gnosis
Gyroscope
Hatom
Hone
HydraDX
IOHK
Maker
Membrane Finance
Morpho
MultiversX
Ojo
Olympus DAO
optimism
Pact
Panvala
Parity
PlatON
Polkadot
PON Network
QuipuSwap
Stakefish
StakerDAO
StakeWise
SundaeSwap
Swaap
Synonym Finance
Tempus blockchain
Term Labs
Tezos
Tinyman
Tracer
Umee
Uniswap
Web3 Foundation
Whiteblock
World Mobile
xBacked
Xfinite
Yieldly
Zivoe
Zorp

Smart contract review ("audit") and formal verification team members

Frequently asked questions about smart contracts

What is the difference between security reviews ("audits") and formal verification?

Formal verification is not the same as a traditional security audit. With formal verification, contract code is verified at the bytecode level using tools developed based on a mathematical model of the EVM. The result is a level of assurance that traditional reviews, limited to reviewing the Solidity code itself, cannot offer with respect to the functional correctness of the code.

During a formal verification engagement, RV formalizes the requirements of the smart contract. That is, all the properties shared become mathematical theorems, proved using RV’s verifier/prover at the EVM bytecode level, making sure all corner cases are rigorously specified and verified. With respect to work allocation, the majority of tasks assigned to verification engineers do not go into the actual verification, but rather in formalizing the actual properties. Security auditors do not do this because they do not possess the required expertise or access to the necessary tools to verify the code against the specs.

RV has discovered issues in all the contracts its verified. Not always issues that can be exploited, but issues clients chose to fix because they are committed to the correctness of their contracts. Contracts that appear correct can be broken with specific inputs at particular corner cases. The human mind simply cannot keep track of all such corner cases, which is why tools based on mathematical models of the computing infrastructure, i.e. the EVM bytecode, are necessary.

How long does it take to formally verify a contract?
It depends. Providing formal verification is a bespoke exercise that is custom to the contract or contracts in question. To lock down both timeline and price, RV and the interested party will engage in a bout of back and forth due diligence that will allow RV to better understand the true intent of your contract, a requirement for any verification project. RV will then provide a work plan that includes incremental tasks and deliverables, itemized cost for each deliverable, and delivery estimate for each deliverable. The work plan can then be modified to best align with your roadmap and/or budget requirements.

Academic papers published by Runtime Verification experts

Tools And Application
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

Daejun Park, Yi Zhang and Grigore Roșu

CAV, 2020

PDF
A Formal Verification Tool for Ethereum VM Bytecode

A Formal Verification Tool for Ethereum VM Bytecode

Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian and Grigore Roșu

ESEC/FSE'18, ACM. 2018.

PDF, Formally Verified Smart Contracts, ESEC/FSE'18, BIB
Semantics-Based Program Verifiers for All Languages

Semantics-Based Program Verifiers for All Languages

Andrei Ștefănescu, Daejun Park, Shijiao Yuwen, Yilong Li and Grigore Roșu

OOPSLA'16, ACM, pp 74-91. 2016

PDF, Matching Logic, DOI, OOPSLA'16, BIB
Theory
Program Verification by Coinduction

Program Verification by Coinduction

Brandon Moore, Lucas Peña and Grigore Roșu

ESOP'18, Springer, pp 589-618. 2018

PDF, Matching Logic, DOI, ESOP'18, BIB
Matching Logic

Matching Logic

Grigore Roșu

LMCS, Volume 13(4), pp 1-61. 2017

PDF, DOI, LMCS, BIB
All-Path Reachability Logic

All-Path Reachability Logic

Andrei Ștefănescu, Ștefan Ciobaca, Radu Mereuță, Brandon Moore, Traian Șerbănuță and Grigore Roșu

RTA'14, LNCS 8560, pp 425-440. 2014

PDF, Matching Logic, DOI, RTA'14, BIB
Formal Semantics
KEVM: A Complete Semantics of the Ethereum Virtual Machine

KEVM: A Complete Semantics of the Ethereum Virtual Machine

Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ștefănescu and Grigore Roșu

CSF 2018, IEEE, pp 204-217. 2018

PDF, KEVM, CSF 2018, BIB
IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Șerbănuță, Virgil Șerbănuță, Daniele Filaretti, Grigore Roșu and Ralph Johnson

Technical Report http://hdl.handle.net/2142/100320, July 2018

PDF, IELE, DOI, BIB