Formal Verification of ERC-Based Smart Contracts: A Systematic Literature Review

Defined as an agreement between multiple parties and systematically executed by a computer code, smart contracts enable trust-less execution without a third party. Despite the trusted implementations that smart contracts offer, including those based on standards, different security problems and vulnerabilities arise during their development and execution. To address these issues, multiple studies have proposed potential solutions, focusing particularly on the verification of smart contracts and considering the standard-based ones using formal verification techniques. However, the sheer amount of research makes it difficult to accurately articulate the state-of-the-art. To tackle this challenge, we propose a systematic literature review that deals with formal verification of ERC-based smart contracts. ERC (Ethereum Request for Comments) standards enable a range of functionalities, such as the creation and management of tokens. Thus, our review provides an overview of ERC standards and examines their related potential issues. Furthermore, we investigate existing solutions presented in 19 relevant studies published between 2019 and July 2023. We analyze and classify approaches to formal modeling, properties' specification and techniques used in the verification of smart contracts. Finally, we discuss the research challenges and suggest some promising future directions to stir research efforts into this area.