Deductive proof of industrial smart contracts using why3

Abstract

In this paper, we use a formal tool that performs deductive verification on industrial smart contracts, which are self-executing digital programs. Because smart contracts manipulate cryptocurrency and transaction information, if a bug occurs in such programs, serious consequences can happen, such as a loss of money. This paper aims to show that a language dedicated to deductive verification, called WhyML, can be a suitable language to write correct and proven contracts. We first encode existing contracts, using the Why3 tool, into WhyML program; next, we formulate specifications to be proven as the absence of RunTime Error and functional properties, then we verify the behaviour of the program using the Why3 system. Finally, we compile the WhyML contracts to the Ethereum Virtual Machine (EVM). Moreover, our approach estimates the cost of gas, which is a unit that measures the amount of computational effort during a transaction.