Smart contracts are programs written in Turing complete languages that can be deployed to specific blockchain platforms. Due to the nature of their application, they can hold and manipulate significant monetary assets, which marks them as tentative targets for attackers. In addition, their execution in blockchain platforms leads to financial costs that need to be managed properly, or significant monetary loss is possible. In this project we investigate the application of formal verification in this context, tackling both safety issues, as well as execution costs, i.e. contracts' gas consumption.