A Survey on Formal Verification for Solidity Smart Contracts

Abstract

One of the 21st century’s hottest topics in the world of IT has been the emergence of what some predict to be the foundation stone for a new era of internet (web 3.0): Blockchain technology. Besides being the backbone of what we come to know as cryptocurrencies, Blockchain’s features make for a bottomless list of possible applications, especially thanks to the concept of smart contracts. This, however, caused Blockchain to be in the limelight of not only interested investors but also malicious users who started hunting for this technology’s vulnerabilities, which resulted in numerous attacks on different Blockchain platforms. In an attempt to mend such loopholes, researchers took an interest in the verification of smart contracts, which are at the heart of Blockchain’s applications. In this survey, we aim to present a general overview of the different axes investigated by researchers towards the verification of smart contracts, while taking a special interest in studies that focus on formal verification, the different approaches they apply and vulnerabilities they target.