This is supplementary material for the paper Secure Smart Contracts with Isabelle/Solidity It contains the Isabelle theory files as well as the corresponding proof document: Utils.thy: A set of general functions and lemmas independent of Solidity. State_Monad: A formalizaton of a state monad with exceptions and non-termination. It provides also a new mode sm for the partial function package. State.thy: A formalization of the Solidity storage model consisting of definitions for storage, memory, calldata, and stack. In addition it contains several useful functions for the different types of stores such as functions to copy data structures from one store to another. Solidity.thy: A formalization of Solidity expressions and statements in terms of our state monad. WP.thy: A weakest precondition calculus and corresponding verification condition generator for our Solidity monads. Unit_tests.thy: A test suite to validate conformance of the semantics to the original Solidity documentation. The test cases were executed using the [Remix IDE](https://remix.ethereum.org/). Contract.thy: An Isabelle/ML implementation of two new commands: `contract` and `invariant` to support the specification of Solidity contracts and verification of invariants in Isabelle. Solidity_Main.thy: Main entry point Token.thy: A formalization of a simple banking contract and verification of a key invariant using Isabelle/Solidity. Casino.thy: A formalization of a casino contract and verification of a key invariant using Isabelle/Solidity. Voting.thy: A formalization of a delegated voting contract and verification of a key invariant using Isabelle/Solidity. isabelle-solidity.pdf: Formal proof document.