Smart contracts are an emerging form of decentralised programs running on blockchains Since the smart contract languages, e g the Ethereum contract language Solidity, are usually Turing-complete languages, smart contracts can support a wide range of application scenarios, one example is to manage assets and properties Similarly to classical sequential programs, smart contracts can be error-prone or contain serious security vulnerabilities, which, nevertheless, can have much more catastrophic consequences than them, for instance, the infamous DAO attack ever caused a 80,000,000 American dollar loss In this talk, I will (1) summarise the security issues in smart contracts, (2) illustrate why and where formal methods can help to guarantee the correctness and security of smart contracts, and (3) report our efforts, progress and preliminary results in this field

郭宇，SECBIT（安比）实验室创始人，中国科学技术大学博士、耶鲁大学访问学者、前中科大副教授，曾任职知名金融科技公司副总裁。在形式化证明与系统软件研究领域深耕多年，也是国内早期关注并参与比特币与区块链技术的科研人员之一。