Smart contracts

Smart contract analysis and verification

We pioneered many of the techniques the community now uses, including the K framework and language-independent verification technology. Formal modeling, analysis, safety, security, validation and verification, applied to contracts and to everything underneath them.

We have 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 consensus protocols, programming languages and virtual machines as well. The K framework is ours.

Interested in reviewing the work to date? It is all in our publications repository.

Analysis and verification packages

Proven expertise in formal verification and assurance.

Design review

Our speciality in formal methods lets us take a critical look at your product's design. Errors in design are the most critical and the most costly to fix, so it is best to catch them early. Our engineers review your specifications and implementation, consulting continuously with your developers, to understand the product, make sure there are no holes or inconsistencies in the design, and discover the properties and invariants the product needs for safe operation. We contribute directly to your specifications where issues are found, which can then be part of the public documentation and lays the foundation for the later steps of a security audit.

Code review

Following design review, our team has a thorough understanding of your product and a completed specification to work from. We systematically review the codebase, making sure it conforms to that specification. Our training in formal methods lets us take a verification-oriented approach to the review, manually proving that the important properties of the product hold for each component of the code. Everything found in the process is documented and reported to your developers in real time.

Security audit report

Following a design review and either a code review or formal verification, we produce a unified report describing the work done with your product. It can be published among our public audit reports as a record of that work. The report includes any design documentation we produced, the properties we specified, a description of the audit scope, every issue discovered over the course of the engagement, and any verification artifacts relevant to the codebase.

Formal modeling

This package applies to any system, including programming languages, virtual machines and protocols, not only to smart contracts. For a smart contract it means formally specifying the contract's business logic to produce a precise, unambiguous and comprehensive model. The model is executable, so it doubles as a reference implementation and supports blackbox test generation. We then validate the critically important properties of that business logic, which is the strongest formal guarantee available for the absence of loopholes. Note that this package does not include formal verification of the contract code itself.

Formal verification

The highest level of guarantee available for a codebase is formal verification: proof that the code will always behave as expected. We translate the properties and specifications discovered during design review into machine-readable specifications via our property-testing framework. On Ethereum that is Kontrol, which expresses verification conditions as Solidity property tests. That makes the verification something we can wire directly into your CI, and something your developers can maintain and extend after the engagement ends.

Discuss a package

How an engagement runs

From the first call to a published report.

Our team reviews your code line by line, checking for bugs, errors, security vulnerabilities and exploits. On top of that manual review we run our own bounded model checking tool, powered by the K framework and its symbolic execution capability.

01
Meet and greet
- You present your company, dive into your contract, and identify requirements.
- RV runs through the available review and verification packages.
- RV introduces a typical engagement from start to finish.
02
Package selection and agreement
- You select the package that best meets your needs.
- RV provides an estimated timeline for delivery of your engagement.
- We sign the contract and you provide the initial deposit.
03
Engagement and report
- RV reviews and/or verifies your code.
- RV drafts a preliminary report and debriefs you on the findings.
- You implement code improvements.
- RV delivers and publishes the final report, with your approval.

Teams we have worked with

Smart contract review and verification team

The full team

Frequently asked

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 built on a mathematical model of the EVM. The result is a level of assurance that traditional reviews, limited to the Solidity code itself, cannot offer about the functional correctness of the code.

During a formal verification engagement we formalize the requirements of the contract: every property shared becomes a mathematical theorem, proved with our verifier at the EVM bytecode level, so all corner cases are rigorously specified and verified. Most of the work assigned to verification engineers does not go into the verification itself but into formalizing the properties. Security auditors do not do this, because they do not have the expertise or the tools to verify code against specs.

We have discovered issues in every contract we have verified. Not always exploitable ones, but issues clients chose to fix because they are committed to the correctness of their contracts. A contract that appears correct can be broken by specific inputs at particular corner cases. The human mind cannot keep track of all of them, which is why tools based on mathematical models of the computing infrastructure are necessary.

How long does it take to formally verify a contract?

It depends. Formal verification is a bespoke exercise, custom to the contracts in question. To pin down both timeline and price, we and the interested party go through some back-and-forth due diligence so we understand the true intent of the contract, which is a requirement for any verification project. We then provide a work plan with incremental tasks and deliverables, an itemized cost for each, and a delivery estimate for each. The plan can be adjusted to fit your roadmap or budget.

Academic papers by RV experts

Tools and application