Exploring and applying smart contract formal verification approaches on the Ethereum platform

As blockchain technology evolves, it is permeating various sectors of the economy. Large numbers of smart contracts are emerging, automating the interaction of participants in the decentralized network. However, their widespread use underscores the need to ensure the security and reliability of smart contract code, especially considering the fact that it can't be changed after deployment. Formal verification methods allow you to mathematically prove that the source code meets the correctness specification, thereby helping to prevent errors and financial losses associated with vulnerabilities in smart contracts. This presentation will analyze approaches to the formal verification of smart contracts on the Ethereum network currently employed in the industry. The review aims to understand the advantages and disadvantages of these approaches, as well as to identify common trends in this field. Furthermore, an example will be given of applying deductive formal verification methods to prove the correctness of voting smart contracts and an automated market maker. Kirill Ziborov Positive Technologies