AN ALGEBRAIC APPROACH TO THE VERIFICATION OF SMART CONTRACTS IN TEAL

Abstract

Blockchain and smart contracts have transformed the modern world. They help ensure security and trust in transactions, revolutionize finance, logistics, healthcare, and many other industries. Smart contracts are based on software code, so they can contain errors that lead to incorrect execution of the contract. Since the area of use of smart contracts is often related to finance, the cost of such errors can be quite high. Also, errors in smart contracts that have already been sent to the network cannot be corrected due to the immutable nature of the blockchain. This problem can be solved through smart contract code analysis, which allows developers to check the correctness of their code and protect it from possible errors and vulnerabilities.

This article proposes the use of insertional modeling to analyze smart contract code for the Algorand blockchain. This blockchain is one of the fastest, low-cost, carbon-negative blockchains that has advanced smart contract capabilities with low transaction fees. The language used to create smart contracts in Algorand is called Transaction Execution Approval Language (TEAL).

In this work, we review existing tools for TEAL code verification and describe the capabilities that each of them provides. Among these tools are Graviton, Tealer, Algo Builder/runtime. In this paper we describe the features of the TEAL language, as well as give examples of writing a smart contract using it.

We offer our method for verification created smart contract. It consists in using the algebraic approach, which is implemented in the scope of the insertion modeling system to verify the smart contract code. This approach will allow us to check the smart contract code for some state reachability and deadlocks.