  A bug or error is a common problem that any software or computer program may
encounter. It can occur from badly writing the program, a typing error or bad
memory management. However, errors can become a significant issue if the unsafe
program is used for critical systems. Therefore, formal methods for these kinds
of systems are greatly required. In this paper, we use a formal language that
performs deductive verification on an Ethereum Blockchain application based on
smart contracts, which are self-executing digital contracts. Blockchain systems
manipulate cryptocurrency and transaction information. Therefore , if a bug
occurs in the blockchain, serious consequences such as a loss of money can
happen. Thus, the aim of this paper is to propose a language dedicated to
deductive verification, called Why3, as a new language for writing formal and
verified smart contracts, thereby avoiding attacks exploiting such contract
execution vulnerabilities. We first write a Why3 smart contracts program; next
we formulate specifications to be proved as absence of RunTime Error properties
and functional properties, then we verify the behavior of the program using the
Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual
Machine (EVM). Moreover, we give a set of generic mathematical statements that
allows verifying functional properties suited to any type of smart contracts
holding cryptocurrency, showing that Why3 can be a suitable language to write
smart contracts. To illustrate our approach, we describe its application to a
realistic industrial use case.
