Paper accepted for SEFM24

Secure Smart Contracts with Isabelle/Solidity


Isabelle/Solidity is a framework for the verification of Solidity smart contracts using Isabelle. It is based on a shallow embedding and provides new commands for Isabelle to specify and verify Solidity contracts.

Isabelle/Solidity is described in our new paper accepted for publication at the 22st International Conference on Software Engineering and Formal Methods. A preprint is available here.