I am glad to share a preprint of our latest work in which we present a denotational semantics of a subset of Solidity and its implementation in Isabelle/HOL. This is a collaboration with Prof. Achim Brucker and will be presented at SEFM 2021.
Check out the preprint to learn more about the details of Solidity.
Dr. Diego Marmsoler 