On the Formal Verification of Smart Contracts

In recent years, Blockchain-based systems have experienced rapid growth. Although these systems are in production, they are not exempt from presenting defects in the design of their elements such as Smart Contracts. Design defects in Smart Contracts lead to inconsistencies and consequently to incorrect operation, which generates problematic situations during and after the execution of the system. In this paper, we describe an overview of main current approaches to formally verify Smart Contracts. Moreover, it is proposed to use Descriptive Logics to verify the consistency of functionality in the designs of Smart Contracts. The balance between expressiveness and computational complexity of Descriptive Logics, allow to model in an unified framework elusive Smart Contract properties, such as temporal and spatial ones. Furthermore, it will allow reliable and efficient verification of these properties.