Towards benchmarking of Solidity verification tools
Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, Franco Sainas
TL;DR
This work addresses the lack of public benchmarks for Solidity verification tools by proposing an open benchmark with 323 verification tasks, a grounded truthset, and an automated toolchain to generate tasks and execute SolCMC and Certora. It provides a comparative analysis of SolCMC and Certora across completeness, soundness, and expressiveness, highlighting that Certora supports more expressive properties while both tools exhibit notable limitations. The study reveals how external calls, EOAs, and reentrancy affect verification outcomes, underscoring the need for robust benchmarks to guide tool selection and drive improvements in Solidity verification technology. By releasing the benchmark openly, the authors aim to foster community collaboration and accelerate progress toward reliable, scalable verification for smart contracts.
Abstract
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.