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