Talk by Diego Marmsoler, University of Exeter
Smart contracts are digital contracts stored on a blockchain that are automatically executed when predetermined terms and conditions are met. Technically, smart contracts are programs which are usually developed in a high-level programming language, the most popular of which being Solidity. Smart contracts are often used to automate financial transactions and thus, vulnerabilities in smart contracts can result in high financial losses. For example, it is estimated that since 2019, more than $5B were lost due to vulnerabilities in smart contracts.
Moreover, once deployed to the blockchain, smart contracts cannot be updated or removed easily. Thus, it is important to “get smart contracts right”, before they are deployed on a blockchain for the very first time.
To this end, we developed Isabelle/Solidity, an embedding of Solidity in Isabelle/HOL which can be used to verify Solidity contracts. So far, Isabelle/Solidity was used to verify the correctness of a Gas optimization program, the soundness of a verification methodology for smart contracts, as well as an implementation of a simple banking dapp (decentralized application).
In this talk I will briefly introduce Isabelle/Solidity, discuss its applications as well as limitations and ongoing projects.