We present a reduction from verification of smart contracts to model checking. A smart contract is a computer program written in a language with constructs that correspond to real-world contracts, such as verified sending ...