A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

翻译：智能合同是一种计算机程序,它使用户能够使其在供应链平台上的行动自动化。鉴于智能合同对支持包括供应链、金融、法律和医疗服务在内的各行业的重要活动具有重要意义,对核查和验证技术的需求很大。然而,绝大多数智能合同缺乏任何正式规格,而这种规格对于确定其正确性至关重要。在本次调查中,我们调查文献中提供的智能合同的正式模型和规格,提出系统概览,以便了解共同趋势。我们还讨论目前用于核实这些财产规格的方法,并找出差距,希望为今后的工作找到有希望的方向。