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

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