Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Announcement: Isabelle/Solidity

Ever wondered how to verify smart contracts written in Solidy? Thanks to our deep embedding of Solidty into Isabelle/HOL, you can now start verifying smart contracts in Isabelle.

Our formalization is available in the Archive of Formal Proofs [1], which can be easily added to Isabelle/HOL. If you want to read a more high-level description of the underlying work, read our conference papers on the topic [2].

References

1. Marmsoler, D. and Brucker, A. D. “Isabelle/Solidity: A Deep Embedding of Solidity in Isabelle/HolArchive of Formal Proofs (2022): URL: http://www.brucker.ch/bibliography/abstract/marmsoler.ea-isabelle-solidity-2022

2. Marmsoler, D. and Brucker, A. D. “A Denotational Semantics of Solidity in Isabelle/HOLSoftware engineering and formal methods (sefm) (2021): URL: http://www.brucker.ch/bibliography/abstract/marmsoler.ea-solidity-semantics-2021

3. Marmsoler, D. and Brucker, A. D. “Conformance Testing of Formal Semantics Using Grammar-Based FuzzingTAP 2022: Tests and proofs (2022): URL: http://www.brucker.ch/bibliography/abstract/marmsoler.ea-conformance-2022