A deep embedding of Solidity in Isabelle/HOL
Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts.
To address the issue of smart contract vulnerabilities we developed Isabelle/Solidity. Isabelle/Solidity is, on the one hand, a deep embedding of an executable denotational semantics for Solidity within the Isabelle/HOL interactive theorem prover. On the other hand, Isabelle/Solidity is an interactive program verification environment for Solidity smart contracts.
We describe Isabelle/Solidity in our latest publication in the journal Formal Aspects of Computing [1].