The still-experimental nature of smart contracts requires us to give adequate attention to the security aspects of these special DApps. Damage resulting from vulnerabilities present in smart contracts can have a significant impact on the entire architecture of the underlying blockchain. In fact, once deployed on the blockchain, smart contracts cannot be edited. The executable code of smart contracts takes the form of bytecode interpreted by a special virtual machine (VM), which, in the case of Ethereum, is Ethereum Virtual Machine (EVM). To check the presence of vulnerabilities within smart contracts, it is possible to perform a code review of the source code, but there are some specific tools that allow even the bytecode produced during the compilation phase to be analyzed.
One of the first tools created for the verification of smart contracts is MAIAN...
