Smart contracts are a very interesting application domain for validation, verification and optimization techniques since (1) they are relatively small in size, hence the application of these techniques scales well, (2) they are valuable (in the corresponding blockchain cryptocurrency), hence software bugs or inefficiencies can cause economical losses, and (3) they require proving new properties to ensure their reliability and efficiency. This talk overviews the main features of smart contracts and discusses our current work on the verification of gas-related and safety properties whose main goals are to save resources, prevent vulnerabilities and avoid potential attacks.