New TCS paper

Created in February 16, 2026

2026

Our paper Type safety for Isabelle/Solidity is finally published in Theoretical Computer Science.

In the paper we verify the consistency of the storage model of Isabelle/Solidity. This includes:

  • A formal definition of type safety for Isabelle/Solidity.
  • A mechanized proof which shows that type safety is preserved by statements.

Abstract. Smart contracts are programs stored on the blockchain that are often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions; thus, bugs can lead to large financial losses. In Solidity, programs have access to different types of stores which can store different types of data. However, data is stored without typing information therefore it is important to ensure that Solidity programs do not compromise type consistency of the data contained in these stores. With this work, we use an existing formal semantics of Solidity to verify type consistency of Solidity programs. To this end, we define type safety in the context of Solidity and prove that it is preserved by the semantics. The definition of type safety as well as its verification is formalized in the proof assistant Isabelle. To the best of our knowledge this is the first attempt to verify this type of property for Solidity.

Link: https://www.sciencedirect.com/science/article/pii/S0304397525005699