Secure Smart Contracts with Isabelle/Solidity

智能合约是存储在区块链上的数字合约，当满足预定的条款和条件时自动执行。它们通常用于自动化金融交易，因此它们具有改变和破坏金融行业的巨大潜力。特别是，据估计，到2030年，bbb和智能合约可以为英国的GDP增加722亿美元，并创造多达70万个新工作岗位。从技术上讲，智能合约是程序，因此它们可能包含错误。然而，由于智能合约通常用于自动化金融交易，利用这些漏洞可能会导致巨大的财务损失。例如，在2016年，智能合约中的一个漏洞被利用，导致大约6000万美元的损失。最近，黑客利用智能合约中的漏洞窃取了6亿美元。总的来说，据估计，自2019年以来，由于智能合约的漏洞，损失了超过50亿美元。这威胁到社会对智能合约的信任，从而限制了它们发展金融科技的潜力，而金融科技是英国经济最有前途的行业之一。然而，不幸的是，即使是严格的测试和审计也不能保证智能合约做它应该做的事情。在最好的情况下，可以在这些技术中找到漏洞，但它们永远不能保证不存在漏洞。因此，通过这个项目，我们将开发工具和技术来支持智能合约的验证，以实现最高程度的可靠性。最后，我们将通过在埃克塞特举办关于区块链正式方法的暑期学校，参与培训下一代智能合约验证专家。

Smart contracts are digital contracts stored on a blockchain that are automatically executed when predetermined terms and conditions are met.They are often used to automate financial transactions and thus they hold great potential to transform and disrupt the financial industry.In particular it is estimated that blockchain and smart contracts can add up to $72.2B to the UK's GDP by 2030 and create up to 700,000 new jobs by 2030.Technically, smart contracts are programs and as such, they may contain bugs.However, since smart contracts are often used to automate financial transactions, exploiting these bugs may result in huge financial damages.In 2016, for example, a vulnerability in a smart contract was exploited, resulting in a loss of approximately $60M.More recently, hackers had exploited a vulnerability in a smart contract to steal $600M.In general, it is estimated that since 2019, more than $5B were lost due to vulnerabilities in smart contracts.This threatens society's trust in smart contracts and thus limits their potential for the development of FinTech, one of the most promising sectors for the UK economy.Unfortunately, however, even rigorous testing and auditing cannot guarantee that a smart contract does what it is supposed to do.In the best case scenario, vulnerabilities can be found with these techniques but they can never guarantee their absence.Thus, with this project, we will develop tools and techniques to support the verification of smart contracts to achieve the highest degree of reliability.Finally, we will engage in training next generation experts in the verification of smart contracts by hosting a summer school on formal methods for blockchains in Exeter.