智能合约的验证形式方法：综述

智能合约是依赖区块链技术的数字合同，旨在使其条款和执行条件无法伪造。智能合约的目的是消除在匿名和已识别参与者之间的商业和贸易中对中介的需求。自2016年以来，智能合约在公共管理、供应链、能源、金融、通信和医疗等多个领域获得了广泛关注。任何在区块链系统上发布后与智能合约互动的人，如果其包含漏洞或错误，将面临风险。因此，需要使用形式化方法，即用于建模、设计和测试软件和硬件系统的数学技术，以确保它们正确构建。本文回顾了应用于智能合约规范和验证的先进形式方法，旨在将故障和漏洞的风险最小化，避免可能造成的成本。同时，我们讨论了与这一新兴研究主题相关的若干挑战和未来研究指导。