Deductive Verification of Smart Contracts with Dafny

TL;DR

This paper introduces a methodology for developing verified smart contracts using Dafny, focusing on correctness, external calls, and re-entrancy, to enhance safety and reduce bugs in blockchain applications.

Contribution

It presents a novel approach to smart contract verification using Dafny, including reasoning about external calls and re-entrancy, with a straightforward translation to Solidity.

Findings

Effective reasoning about external calls and re-entrancy in smart contracts.

Potential for safer smart contract development with formal verification.

Feasibility of translating Dafny code to Solidity for deployment.

Abstract

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.