What Is Formal Verification of Smart Contracts?

This article is a community submission. The author is David Tarditi, VP of Engineering at CertiK, a Web3 smart contract auditing firm.

Views in this article are of the contributor/author and do not necessarily reflect those of Binance Academy.

TL;DR

Formal verification of smart contracts ensures they are free from bugs, vulnerabilities, and other unintended behavior. It involves a human expert presenting the smart contract's logic as mathematical statements, then running them through an automated process that checks the actual logic against models of the contract’s expected behavior. The combination of formal verification and manual auditing provides a comprehensive evaluation of a smart contract's security.

Introduction

Smart contracts are computer programs deployed on a blockchain that run automatically when certain conditions are met. They can range from simple to extremely complex, and can hold assets worth millions or even billions of dollars.  

Security vulnerabilities in smart contract code can have devastating consequences, including theft of all the assets held by a smart contract. In 2021, automated market maker (AMM) Uranium Finance had $50 million stolen because of a single typo in a smart contract.

Also in 2021, Compound Finance gave out $80 million in unearned rewards because of a single character mistake. In 2022, $320 million was stolen from the Wormhole Bridge because of a bug in one of its smart contracts.

It’s important to get the smart contract program right the first time. Smart contracts are open-source, meaning the code is publicly available once a contract is deployed. If a hacker finds a bug, they can take advantage of it immediately. In addition, patching security vulnerabilities over time is not an option, as a smart contract’s code typically cannot be modified after deployment.

How Does Smart Contract Verification Work?  

Formal verification of smart contracts works by presenting the logic and desired behavior of smart contracts as mathematical statements. Auditors then use automated tools to check if these statements are correct.

The process involves:

1. Defining the specifications and desired properties of a contract in formal language.

2. Translating the contract’s code into a formal representation, such as mathematical models or logic.

3. Using automated theorem provers or model checkers to validate the contract’s specifications and properties.

4. Repeating the verification process to find and fix any errors or deviations from the desired properties.

Why Smart Contract Verification Is Important

The use of mathematical reasoning helps to ensure that formally verified smart contracts are free from bugs, vulnerabilities, and other unintended behavior. It also helps to increase trust and confidence in the contract, as its properties have been rigorously proven to be correct. 

Below are some examples of how smart contract verification has helped prevent significant financial loss and other disastrous outcomes.  

Uniswap

Uniswap is a well-known AMM. When the Uniswap V1 smart contract was developed, it was formally verified. Prior to its release, this formal verification found and fixed rounding errors that could have led to Uniswap V1 being drained of funds. 

Balancer

Balancer V2 is also an AMM that was formally verified. Formal verification found and fixed an incorrect fee calculation involving flash loan functionality in the smart contract, which could have made the exchange vulnerable to theft.

SafeMoon

SafeMoon V1 contained a subtle bug found by formal verification after it was deployed. It was possible for an owner to renounce ownership of the contract and then reacquire it, if certain operations were done before renouncing ownership.

This bug was missed in most manual audits of SafeMoon V1 forks because finding it required analyzing specific combinations of program variable values. This is something that’s easy for humans to miss, and easy for a machine to pick up.

How Formal Verification and Manual Auditing Work Together

Formal verification provides a systematic and automated way to check a contract's logic and behavior against its desired properties. This makes it easier to identify and fix any potential errors or bugs. It is especially useful for finding complex and subtle issues that may be difficult to detect through manual inspection.

Manual auditing involves the expert review of a contract's code, design, and deployment. The auditor uses their experience and expertise to identify security risks and evaluate the contract's overall security posture. They can also confirm that the formal verification process was performed correctly, and check for any issues that may not be detectable by automated tools. 

Combining formal verification and manual auditing provides a comprehensive and thorough evaluation of a smart contract's security. This increases the chances of finding and fixing any vulnerabilities. The result is a defense-in-depth approach to security that leverages the unique capabilities of both humans and machines. 

Closing Thoughts

To ensure the security of smart contracts, it is essential to use both formal verification and manual auditing to ensure a comprehensive and thorough evaluation of a smart contract's security posture.

While formal verification can be resource-intensive, it is a worthwhile investment for contracts with high value or high-risk factors. Ultimately, prioritizing security and ensuring smart contracts are free from bugs, vulnerabilities, and unintended behavior is vital.

Further Reading

• What Are Smart Contracts?

• What Is a Smart Contract Security Audit?

Disclaimer and Risk Warning: This content is presented to you on an “as is” basis for general information and educational purposes only, without representation or warranty of any kind. It should not be construed as financial, legal or other professional advice, nor is it intended to recommend the purchase of any specific product or service. You should seek your own advice from appropriate professional advisors. Where the article is contributed by a third party contributor, please note that those views expressed belong to the third party contributor, and do not necessarily reflect those of Binance Academy. Please read our full disclaimer here for further details. Digital asset prices can be volatile. The value of your investment may go down or up and you may not get back the amount invested. You are solely responsible for your investment decisions and Binance Academy is not liable for any losses you may incur. This material should not be construed as financial, legal or other professional advice. For more information, see our Terms of Use and Risk Warning.