Smart Contract Verification

A smart contract is a computer program whose effects — often transfers of cryptocurrency — are irreversible. Because the program is itself stored irreversibly and is always visible, you can always know exactly what those effects will be.

Or can you?

Imagine a smart contract managing a vast sum of money. It’s visible to anyone in the world. If that anyone finds a bug, it can’t be fixed. (Irreversible, remember?) There are a lot of people highly motivated to find bugs that let them drain accounts. They’ve often succeeded. So a company deploying a smart contract is essentially betting that their one or few programmers will be better at not making mistakes than the entire world is at finding and exploiting them.

Because of the special characteristics of smart contracts, and our previous work on the Ethereum Virtual Machine and Cardano’s IELE, Runtime Verification can prove smart contracts correct for a cost comparable to a manual audit.

Work with us


A formal smart contract verification engagement from start to finish

Initial Meet & Greet

  • Present RV’s formal verification philosophy and process

  • Introduce client’s business & reason(s) for formal verification services

  • Initial review of your project’s requirements

  • Q&A to collect information for formal proposal

Prepare & Deliver formal project proposal

  • Review & audit of contract(s)

  • Identify goals, priorities, and milestones for project

  • Provide estimated timeline and cost estimate for delivery of project

Proposal acceptance & kickoff

  • Review milestones, deliverables, and timeline

  • Review project management roles and responsibilities

  • Review communication and collaboration plan

Project Engagement “Live”

  • FORMALIZE contract as a mathematical specification

  • IDENTIFY & CONFIRM opportunities for code improvement

  • REFINE the specification to match the target virtual machine (VM)

  • COMPILE & TEST the smart contract from the language it was written to the VM bytecode

  • VERIFY the resulting bytecode satisfies the contract’s refined specifications

Final report

  • Delivery of formal report to client including project repo

  • Debrief client on project’s findings


Note: Generally speaking, simple, lightweight verification engagements cost the same as a normal smart contract human auditor, but the functional correctness analysis is of course much deeper, taking into account all the semantic details of the generated binary. More complex engagements, which require us to formally specify and validate the protocol in addition to verifying the code, can run mid-to-high six figures.

Let us show you How Formal Verification of Smart Contracts Works and describe the Formal Verification of ERC-20 Contracts.



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 .






Research papers published by Runtime Verification

Newsletter

Your email is safe with us

Working with us

What interests you?

Your email

Your phone number

Thank you!

We'll respond to your request within 48 hours

Recent publication

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

All publications