Smart Contract Audits and Verification


Why work with us

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.


Security reviews ("audits") 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.

  7-14 days

Traditional Security Review ("Audit")

This package provides code review and security assessment of the smart contract, including the following:

  • Common anti-pattern analysis: Check if the code is vulnerable to known security issues and attack vectors such as reentrancy, transaction reordering, and overflows. Please check out our curated list of security vulnerabilities.

  • Software engineering practice evaluation: Evaluate test coverage and inheritance structure, identify code smells (with refactoring suggestion), and detect frequent programming mistakes.

  • Business logic review: Identify loopholes in business logic, and/or inconsistency between the logic and the implementation.

Gnosis

Contact Us

  14-30 days

Tool-based Code Analysis

This package includes but also expands on what’s available in the Traditional Security Review ("Audit") by employing multiple review and/or verification tools - including RV’s own bounded model checker - to review a contract. Additional benefits include the following:

  • Symbolically execute the EVM bytecode of the contract to systematically search for unexpected, possibly exploitable, behaviors at the bytecode level, which can result from quirks or bugs in the EVM or the Solidity/Vyper compiler itself.

  • Measure existing test code coverage and provide “whitebox testing” to improve coverage. The resulting test suite can unveil hidden bugs and support regression testing if/when the contract is updated.

Uniswap

Contact Us

  30-90 days

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.

Bihu   |   ERC20-K   |   ERC777-K   |   Uniswap

Contact Us

  30-90 days

Formal Verification

Like formal modeling, formal verification can also be applied to any system. For smart contracts, this package includes and further refines the Traditional Security Review ("Audit") and Formal Modeling packages, offering formal verification of the contract's EVM bytecode against its formal model/specification, thus eliminating any concerns of potential compiler errors. Specifically:

  • Refine the contract’s high-level formal specification to the bytecode-level to take into account the specifics of the underlying EVM.

  • Formally verify the EVM bytecode of the contract against the refined formal specification. This package provides the ultimate formal guarantee for the correctness of your system or smart contract, and incorporates the best techniques and practices developed by the formal methods community.

Bihu   |   Casper FFG   |   ERC20   |   Gnosis

Contact Us

How smart contract reviews ("audits") 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.

For verification we first formalize your contract as a mathematical specification. This often requires several rounds of discussions and meetings. Next, we refine the specification to match the target low-level virtual machine. We then compile the smart contract from its high-level language (e.g., Solidity, Vyper, Plutus) to VM bytecode. We can then prove whether the bytecode satisfies the refined specification.

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

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


Let’s Get Started

Interested in potentially engaging RV’s smart contract verification services? Please complete the form below. If you prefer email, send your request to .



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