Generating Formal Specifications for Smart Contracts from Textual Descriptions in Natural Language

Abstract

The increasing adoption of smart contracts in decentralized finance (DeFi) and in other areas has led to a growing need for robust and error-free code. This paper addresses this challenge by introducing a grammar-based approach for generating formal specifications from textual descriptions in natural language, specifically post-conditions for ERC20 functions of Solidity smart contracts. Particularly, our approach allows developers to transform natural language descriptions into formal specifications, and vice versa (bidirectional). Thus, developers can automatically derive postconditions from comments to verify conformance, or even generate textual descriptions for complex formal annotations in existing smart contracts to improve legibility.