Formal Modeling and Verification of Smart Contracts

Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an agreement on the contents of the contract and perform the contracts according to the behaviors written in certain computer algorithms. It not only needs to make sure about the correctness of smart contracts code, but also should provide a credible contract code execution environment. Blockchain provides a trusted execution and storage environment for smart contracts by the distributed secure storage, consistency verification and encryption technology. Current challenge is how to assure that smart contract can be executed as the parties' willingness. This paper introduces formal modeling and verification in formal methods to make smart contract model and verify the properties of smart contracts. Formal methods combined with smart contracts aim to reduce the potential errors and cost during contract development process. The description of a general and formal smart contract template is provided. The tool of model checking, SPIN, is used to verify the correctness and necessary properties for a smart contract template. The research shows model checking will be useful and necessary for smart contracts.