Deductive verification of smart contracts with Dafny

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 for 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 Ethereum Virtual Machine bytecode, the results we obtain from the Dafny code can reasonably be assumed to translate to contracts written in languages like Solidity. As a result our approach can readily be used to develop and deploy safer contracts.