Deductive Verification of Smart Contracts with Dafny
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.
Cite
@article{arxiv.2208.02920,
title = {Deductive Verification of Smart Contracts with Dafny},
author = {Franck Cassez and Joanne Fuller and Horacio Mijail Anton Quiles},
journal= {arXiv preprint arXiv:2208.02920},
year = {2022}
}