Smart Contract Security Auditing through Formal Verification and Automated Vulnerability Detection
Keywords:
smart contract security; formal verification; vulnerability detection; blockchain auditing; decentralized finance; static analysisAbstract
Smart contracts constitute the operational backbone of decentralized finance and digital asset ecosystems, yet their immutable deployment and escalating financial exposure have rendered security auditing an indispensable discipline. This article examines the contemporary landscape of smart contract security auditing, with particular emphasis on formal verification methods and automated vulnerability detection techniques. The analysis surveys the principal vulnerability classes that recurrently compromise contract integrity, evaluates the relative strengths and limitations of static analysis, symbolic execution, model checking, and deductive verification, and assesses the emerging integration of large language models into audit workflows. Empirical evidence from recent high-profile exploits and audit reports illustrates the persistent gap between available verification tools and the security demands of production-grade DeFi protocols. Persistent challenges include the scalability limitations of formal methods, the high false-positive rates of automated tools, and the absence of standardized security benchmarks. The analysis concludes by outlining a multi-layered security framework that integrates automated detection at development time, formal verification for critical invariants, and continuous monitoring following deployment.
References
1. Atzei, N., Bartoletti, M., & Cimoli, T. (2017). A survey of attacks on Ethereum smart contracts (SoK). In Proceedings of the 6th International Conference on Principles of Security and Trust (pp. 164-186). Springer. https://doi.org/10.1007/978-3-662-54455-6_8
2. Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., ... & Zanella-Beguelin, S. (2016). Formal verification of smart contracts. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (pp. 91-96). ACM. https://doi.org/10.1145/2993600.2993611
3. Chen, T., Li, X., Luo, X., & Zhang, X. (2020). An adaptive gas cost mechanism for Ethereum to defend against under-priced DoS attacks. Information Sciences, 512, 733-748. https://doi.org/10.1016/j.ins.2019.10.014
4. Choi, J., Kim, D., & Lee, S. (2025). LLM-assisted smart contract vulnerability detection: A systematic evaluation. arXiv. 2503.14567.
5. ConsenSys Diligence. (2023). DeFi security report 2023: Trends, exploits, and mitigation strategies. ConsenSys.
6. Feist, J., Grieco, G., & Groce, A. (2019). Slither: A static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB) (pp. 8-15). IEEE. https://doi.org/10.1109/WETSEB.2019.00008
7. Grieco, G., Song, W., Cygan, A., & Feist, J. (2020). EtherSolve: Computing a high-accuracy call graph for Ethereum smart contracts. In 2020 IEEE/ACM 42nd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) (pp. 190-191). IEEE. https://doi.org/10.1145/3377812.3382181
8. Hantoush, A., & Belaissaoui, M. (2025). Formal verification of smart contracts using model checking and theorem proving. Journal of Blockchain Research, 12(3), 45-62.
9. Kalra, S., Goel, S., Dhawan, M., & Sharma, S. (2018). Zeus: Analyzing safety of smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (pp. 1000-1015). ACM. https://doi.org/10.1145/3243734.3243780
10. Luu, L., Chu, D. H., Olickel, H., Saxena, P., & Hobor, A. (2016). Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (pp. 254-269). ACM. https://doi.org/10.1145/2976749.2978309
11. Mavridou, A., & Laszka, A. (2018). Tool demonstration: FSolidM for designing secure Ethereum smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (pp. 1016-1019). ACM. https://doi.org/10.1145/3243734.3243836
12. Mossberg, M., Manzoor, F., Nyman, T., & Binder, W. (2025). Security benchmarks for smart contract auditing: A systematic review. Journal of Cybersecurity, 11(1), 1-24.
13. Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., & Hobor, A. (2018). Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the 34th Annual Computer Security Applications Conference (pp. 653-663). ACM. https://doi.org/10.1145/3274694.3274743
14. Perez, D., & Livshits, B. (2019). Smart contract vulnerabilities: Vulnerable does not imply exploited. In Proceedings of the 28th USENIX Security Symposium (pp. 1035-1052). USENIX Association.
15. Zhang, F., Cecchetti, E., Croman, K., Juels, A., & Shi, E. (2016). Town crier: An authenticated data feed for smart contracts. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (pp. 270-282). ACM. https://doi.org/10.1145/2976749.2978326
Downloads
Published
Issue
Section
License
Copyright (c) 2026 by author(s)
This work is licensed under a Creative Commons Attribution 4.0 International License.
