Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been proliferating almost since the inception of Ethereum, only in the last few years we have seen verification tools capable of proving that a contract respects some desirable properties. An open issue is how to evaluate and compare the effectiveness of these tools: indeed, the existing benchmarks for general-purpose programming languages cannot be adapted to Solidity, given substantial differences in the programming model and in the desirable properties. We address this problem by proposing an open benchmark for Solidity verification tools. By exploiting our benchmark, we compare two leading tools, SolCMC and Certora, discussing their completeness, soundness and expressiveness limitations.

翻译：智能合约的形式化验证已成为学术与工业研究的热点，其驱动力源于去中心化应用所管理资产价值的持续增长，以及由此引发的攻击者篡改动机。当前合约验证领域的研究主要围绕Solidity展开，这是以太坊及其他主流区块链所支持的主要高级语言。尽管自以太坊诞生以来，针对Solidity的缺陷检测工具便层出不穷，但直到最近几年，才出现了能够证明合约满足特定属性的验证工具。目前面临的一个开放性问题是如何评估并比较这些工具的有效性：由于Solidity在编程模型与目标属性方面存在显著差异，现有通用编程语言的基准测试无法直接迁移应用。针对这一问题，我们提出了一种面向Solidity验证工具的开源基准测试。通过该基准测试，我们对SolCMC与Certora两大主流工具进行了对比分析，深入探讨了它们在完备性、可靠性及表达能力方面的局限性。