Modeling and Verification of Solidity Smart Contracts with the B Method

Smart contracts written using the Solidity programming language of the Ethereum platform are well-known to be subject to bugs and vulnerabilities, which already have led to the loss of millions of dollars worth of assets. Since smart contract code cannot be updated to patch security flaws, reasoning about smart contract correctness to ensure the absence of vulnerabilities before their deployment is of the utmost importance. In this paper, we present a formal approach for generating correct smart contracts from B specification that verify safety properties. Our approach consists of two phases: first a smart contract and its properties are specified and verified in B, then a set of rules we defined are applied to generate the correct smart contract code in Solidity. The approach is implemented in a tool that can generate Solidity contract from a proven B project. The whole approach is demonstrated by a case study on the ERC-20 (Ethereum Request for Comments 20) Wrapped Ether (WETH) contract, which is abstractly specified in B, with invariants stating correctness properties, modeled checked with ProB for temporal properties, implemented in B0, proven correct, and automatically translated into a Solidity contract.