Comparative Analysis of Hoare Logic-Based Formal Verification Tools for Solidity Smart Contracts
DOI:
https://doi.org/10.5753/jserd.2025.5061Keywords:
Smart Contracts, Solidity, solc-verify, SMTChecker, VeriSmart, CertoraAbstract
Formal verification of smart contracts is widely regarded as an effective method for ensuring correctness and security properties across all possible executions. Its practical relevance has been driven by the availability of automatic verification tools that discharge intricate proofs. Another area of growing interest is the integration of specification paradigms - for example, combining Hoare-logic–style specifications (pre/postconditions and invariants) with SMT and symbolic reasoning - so that each technique can precisely capture complementary aspects of contract behavior. In this article we present a comparative analysis of four leading Solidity verification tools - solc-verify, SMTChecker, VeriSmart and the Certora Prover - and define what is meant here by a formal verification tool: a system that provides mathematically rigorous proofs that stated properties hold for every possible execution of a contract. We also describe a consistent evaluation framework that considers the Solidity version support, the preservation of the original contract structure, the local execution capability, the verification time, and the modeling-language requirements, among other criteria. We used the ERC-20 token standard as a benchmark and applied this framework to obtain empirical evidence of each tool’s capabilities and limitations. Our results expose substantial variability in the tools performances that undermines their trustworthiness in practice and highlights a gap between an academic tool capabilities and the industrial requirements. Finally, we discuss how these findings can inform developers and researchers in selecting appropriate verification tools, thereby contributing to improved smart contract security and reliability.
Downloads
References
Almakhour, M., Sliman, L., Samhat, A. E., and Mellouk, A. (2020). Verification of smart contracts: A survey. Pervasive and Mobile Computing, 67:101227.
Alt, L. and Reitwiessner, C. (2018a). SMT-based verification of solidity smart contracts. In International symposium on leveraging applications of formal methods, pages 376–388. Springer.
Alt, L. and Reitwiessner, C. (2018b). SMT-based verification of solidity smart contracts. In International Symposium on Leveraging Applications of Formal Methods, pages 376–388. Springer.
Ante, L. (2020). Smart contracts on the blockchain – a bibliometric analysis and review. SRPN: Information Technology (Topic).
Bartoletti, M., Crafa, S., and Lipparini, E. (2025). Formal verification in solidity and move: insights from a comparative analysis. arXiv preprint arXiv:2502.13929.
Bartoletti, M., Fioravanti, F., Matricardi, G., Pettinau, R., and Sainas, F. (2024). Towards benchmarking of solidity verification tools. In FMBC@CAV.
Besbas, A., Ailane, A., Kahloul, L., Slatnia, S., and Bourekkache, S. (2024). On the formal verification of smart contracts and blockchain: Challenges and future directions. In 2024 4th International Conference on Embedded & Distributed Systems (EDiS), pages 213–217. IEEE.
Cadar, C., Godefroid, P., Khurshid, S., Păsăreanu, C. S., Sen, K., Tillmann, N., and Visser, W. (2011). Symbolic execution for software testing in practice: preliminary assessment. 2011 33rd International Conference on Software Engineering (ICSE), pages 1066–1071.
Certora.com (2024). The Certora Prover. [link].
DappHub (2024). KLab: A tool for generating and debugging proofs in the K Framework. [link].
de Moura, L. M. and Bjørner, N. S. (2009). Satisfiability modulo theories: An appetizer. In Brazilian Symposium on Formal Methods.
ERCX (2024). ERCx: Property testing for ERC tokens. [link].
Ethereum.org (2024). ERC-20 Token Standard. [link].
Fedyukovich, G., Prabhu, S., Madhukar, K., and Gupta, A. (2018). Solving constrained horn clauses using syntax and data. 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1–9.
Fekih, R. B., Lahami, M., Bradai, S., and Jmaiel, M. (2025). Formal verification of erc-based smart contracts: A systematic literature review. IEEE Access.
Fekih, R. B., Lahami, M., Jmaiel, M., and Bradai, S. (2023). Formal verification of smart contracts based on model checking: An overview. In 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pages 1–6. IEEE.
Garfatta, I., Klai, K., Gaaloul, W., and Graiet, M. (2021). A survey on formal verification for solidity smart contracts. In Proceedings of the 2021 Australasian Computer Science Week Multiconference, ACSW ’21, New York, NY, USA. Association for Computing Machinery.
Hajdu, Á. and Jovanović, D. (2019). solc-verify: A modular verifier for solidity smart contracts. In Working conference on verified software: theories, tools, and experiments, pages 161–179. Springer.
Happersberger, V., Jäkel, F.-W., Knothe, T., Pignolet, Y.-A., and Schmid, S. (2023). Comparison of ethereum smart contract analysis and verification methods. In European Symposium on Research in Computer Security, pages 344–358. Springer.
Hildenbrandt, E., Saxena, M., Zhu, X., Rodrigues, N., Daian, P., Guth, D., and Roşu, G. (2017). Kevm: A complete semantics of the ethereum virtual machine.
Kulik, T., Dongol, B., Larsen, P. G., Macedo, H. D., Schneider, S., Tran-Jørgensen, P. W. V., and Woodcock, J. (2021). A survey of practical formal methods for security. Formal Aspects of Computing, 34:1 – 39.
Le Goues, C., Leino, K. R. M., and Moskal, M. (2011). The Boogie verification debugger (tool paper). In Software Engineering and Formal Methods: 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings 9, pages 407–414. Springer.
Liu, Y., Xue, Y., Wu, D., Sun, Y., Li, Y., Shi, M., and Liu, Y. (2024). PropertyGPT: LLM-driven formal verification of smart contracts through retrieval-augmented property generation. arXiv preprint arXiv:2405.02580.
Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., and Dinaburg, A. (2019). Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186–1189. IEEE.
Mota, A., Yang, F., and Teixeira, C. (2023). Formally verifying a real world smart contract. arXiv preprint arXiv:2307.02325.
Moura, L. d. and Bjørner, N. (2008). Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer.
RuntimeVerification (2024). Kontrol formal verification tool. [link].
So, S., Lee, M., Park, J., Lee, H., and Oh, H. (2020). VeriSmart: A highly precise safety verifier for Ethereum smart contracts. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1678–1694. IEEE.
Soliditylang.org (2024a). SMTChecker. [link].
Soliditylang.org (2024b). Solidity language. [link].
Szabo, N. (1997). The idea of smart contracts. Nick Szabo’s papers and concise tutorials, 6(1):199.
Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., and Li, Z. (2021). A survey of smart contract formal specification and verification. ACM Computing Surveys (CSUR), 54(7):1–38.
Wei, Z., Sun, J., Zhang, Z., Zhang, X., Li, M., and Zhu, L. (2023). A comparative evaluation of automated analysis tools for solidity smart contracts. ArXiv, abs/2310.20212.
Wood, G. (2014). Ethereum: A secure decentralised generalised transaction ledger.
Zhang, Z., Zhang, B., Xu, W., and Lin, Z. (2023). Demystifying exploitable bugs in smart contracts. 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), pages 615–627.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2025 Alexandre Mota, Manoel Villarim, Juliano Iyoda, Márcio Cornélio
This work is licensed under a Creative Commons Attribution 4.0 International License.
