  We present a methodology to develop verified smart contracts. We write smart
contracts, their specifications and implementations in the
verification-friendly language Dafny. In our methodology the ability to write
specifications, implementations and to reason about correctness is a primary
concern. We propose a simple, concise yet powerful solution to reasoning about
contracts that have external calls. This includes arbitrary re-entrancy which
is a major source of bugs and attacks in smart contracts. Although we do not
yet have a compiler from Dafny to EVM bytecode, the results we obtain on the
Dafny code can reasonably be assumed to hold on Solidity code: the translation
of the Dafny code to Solidity is straightforward. As a result our approach can
readily be used to develop and deploy safer contracts.
