{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T19:38:17Z","timestamp":1773171497128,"version":"3.50.1"},"reference-count":47,"publisher":"MDPI AG","issue":"8","license":[{"start":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T00:00:00Z","timestamp":1754611200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62362033"],"award-info":[{"award-number":["62362033"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61962020"],"award-info":[{"award-number":["61962020"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["jxsq2023201009"],"award-info":[{"award-number":["jxsq2023201009"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["20224ACB202006"],"award-info":[{"award-number":["20224ACB202006"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["20244BCE52146"],"award-info":[{"award-number":["20244BCE52146"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Double Thousand Talent Plan of Jiangxi Province","award":["62362033"],"award-info":[{"award-number":["62362033"]}]},{"name":"Double Thousand Talent Plan of Jiangxi Province","award":["61962020"],"award-info":[{"award-number":["61962020"]}]},{"name":"Double Thousand Talent Plan of Jiangxi Province","award":["jxsq2023201009"],"award-info":[{"award-number":["jxsq2023201009"]}]},{"name":"Double Thousand Talent Plan of Jiangxi Province","award":["20224ACB202006"],"award-info":[{"award-number":["20224ACB202006"]}]},{"name":"Double Thousand Talent Plan of Jiangxi Province","award":["20244BCE52146"],"award-info":[{"award-number":["20244BCE52146"]}]},{"name":"Natural Science Foundation of Jiangxi Province","award":["62362033"],"award-info":[{"award-number":["62362033"]}]},{"name":"Natural Science Foundation of Jiangxi Province","award":["61962020"],"award-info":[{"award-number":["61962020"]}]},{"name":"Natural Science Foundation of Jiangxi Province","award":["jxsq2023201009"],"award-info":[{"award-number":["jxsq2023201009"]}]},{"name":"Natural Science Foundation of Jiangxi Province","award":["20224ACB202006"],"award-info":[{"award-number":["20224ACB202006"]}]},{"name":"Natural Science Foundation of Jiangxi Province","award":["20244BCE52146"],"award-info":[{"award-number":["20244BCE52146"]}]},{"name":"Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project","award":["62362033"],"award-info":[{"award-number":["62362033"]}]},{"name":"Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project","award":["61962020"],"award-info":[{"award-number":["61962020"]}]},{"name":"Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project","award":["jxsq2023201009"],"award-info":[{"award-number":["jxsq2023201009"]}]},{"name":"Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project","award":["20224ACB202006"],"award-info":[{"award-number":["20224ACB202006"]}]},{"name":"Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project","award":["20244BCE52146"],"award-info":[{"award-number":["20244BCE52146"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>Smart contracts, as a critical application of blockchain technology, significantly enhance its programmability and scalability, offering broad application prospects. However, frequent security incidents have resulted in substantial economic losses and diminished user trust, making security issues a key challenge for further development. Since smart contracts cannot be modified after deployment, flaws in their design or implementation may lead to severe consequences. Therefore, rigorous pre-deployment verification of their correctness is particularly crucial. This paper explores the symmetry in control flows and state transitions of Solidity smart contracts and leverages this inherent structural symmetry to develop a normalized state transition model based on a finite state machine. The FSM model is subsequently formalized into a Promela model with the Spin model checker. By integrating manually defined Linear Temporal Logic formulas with those generated by Smart Pulse, the Promela model is formally verified in Spin to ensure the correctness and security of smart contracts. This approach establishes a systematic verification framework, providing effective support to enhance the reliability and security of smart contracts.<\/jats:p>","DOI":"10.3390\/sym17081275","type":"journal-article","created":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T11:41:53Z","timestamp":1754653313000},"page":"1275","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Solidity Smart Contracts via Automata Theory"],"prefix":"10.3390","volume":"17","author":[{"given":"Meihua","family":"Xiao","sequence":"first","affiliation":[{"name":"School of Information and Software Engineering, East China Jiaotong University, Nanchang 330013, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yangping","family":"Xu","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, East China Jiaotong University, Nanchang 330013, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongtuo","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, East China Jiaotong University, Nanchang 330013, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ke","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, East China Jiaotong University, Nanchang 330013, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sufen","family":"Yan","sequence":"additional","affiliation":[{"name":"Jiangxi Provincial Party School of CPC, Nanchang 330108, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li","family":"Cen","sequence":"additional","affiliation":[{"name":"International Education College, Jiangxi University of Software Professional Technology, Nanchang 330103, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2025,8,8]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Yaga, D., Mell, P., Roby, N., and Scarfone, K. (2019). Blockchain technology overview. arXiv.","DOI":"10.6028\/NIST.IR.8202"},{"key":"ref_2","unstructured":"Gavin, W. (2025, June 12). Ethereum: A Secure Decentralised Generalised Transaction Ledger. Available online: https:\/\/mholende.win.tue.nl\/seminar\/references\/ethereum_yellowpaper.pdf."},{"key":"ref_3","unstructured":"Etherscan (2025, June 12). The Ethereum Blockchain Explorer. Available online: https:\/\/etherscan.io."},{"key":"ref_4","first-page":"199","article-title":"The idea of smart contracts","volume":"6","author":"Szabo","year":"1997","journal-title":"Nick Szabo\u2019s Pap. Concise Tutor."},{"key":"ref_5","unstructured":"Andreas, M., and Gavin, W. (2018). Mastering Ethereum: Building Smart Contracts and Dapps, O\u2019Reilly Media."},{"key":"ref_6","unstructured":"BlockCAT (2025, June 12). On the Parity Multi-Sig Wallet Attack. Available online: https:\/\/medium.com\/blockcat\/on-the-parity-multi-sig-wallet-attack-83fb5e7f4b8c."},{"key":"ref_7","unstructured":"Pretrov, S. (2025, June 12). Another Parity Wallet Hack Explained. Available online: https:\/\/medium.com\/@Pr0Ger\/another-parity-wallet-hack-explained-847ca46a2e1c."},{"key":"ref_8","unstructured":"Wikipedia (2025, June 12). Poly Network Exploit. Available online: https:\/\/en.wikipedia.org\/wiki\/Poly_Network_exploit."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., and Stefanescu, A. (2018, January 9\u201312). KEVM: A complete formal semantics of the Ethereum virtual machine. Proceedings of the 2018 IEEE 31st Computer Security Foundations Symposium (CSF), Oxford, UK.","DOI":"10.1109\/CSF.2018.00022"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, M., Dhawan, M., and Sharma, S. (2018, January 18\u201321). Zeus: Analyzing safety of smart contracts. Proceedings of the Network and Distributed System Security Symposium (NDSS), San Diego, CA, USA.","DOI":"10.14722\/ndss.2018.23082"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., and Vechev, M. (2020, January 18\u201321). Verx: Safety verification of smart contracts. Proceedings of the 2020 IEEE Symposium on Security and Privacy, San Francisco, CA, USA.","DOI":"10.1109\/SP40000.2020.00024"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"106762","DOI":"10.1016\/j.infsof.2021.106762","article-title":"iContractML 2.0: A domain-specific language for modeling and deploying smart contracts onto multiple blockchain platforms","volume":"144","author":"Hamdaqa","year":"2022","journal-title":"Inf. Softw. Technol."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"33465","DOI":"10.1109\/ACCESS.2022.3162227","article-title":"Solidity Code Generation from UML State Machines in Model-Driven Smart Contract Development","volume":"10","author":"Jurgelaitis","year":"2022","journal-title":"IEEE Access"},{"key":"ref_15","unstructured":"Ethereum (2025, June 12). Solidity Documentation. Available online: https:\/\/docs.soliditylang.org\/en\/v0.8.11."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Dolev, S., and Wang, Z. (2020, January 24\u201327). Sodsmpc: Fsm based anonymous and private quantumsafe smart contracts. Proceedings of the 2020 IEEE 19th International Symposium on Network Computing and Applications (NCA), Cambridge, MA, USA.","DOI":"10.1109\/NCA51143.2020.9306699"},{"key":"ref_17","unstructured":"Volland, F. (2025, June 12). State Machine: A Compilation of Patterns and Best Practices for the Smart Contract Programming Language.2024. Available online: https:\/\/fravoll.github.io\/solidity-patterns\/state_machine.html."},{"key":"ref_18","unstructured":"Mavridou, A., and Laszka, A. (March, January 26). Designing secure ethereum smart contracts: A finite state machine based approach. Proceedings of the International Conference on Financial Cryptography and Data Security, Nieuwpoort, Curacao."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., and Dubey, A. (2019, January 18\u201322). Verisolid: Correct-by-design smart contracts for Ethereum. Proceedings of the Financial Cryptography and Data Security-23rd International Conference (FC 2019), Frigate Bay, Saint Kitts and Nevis. Revised Selected Papers.","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Liao, Z., Hao, S., Nan, Y., and Zheng, Z. (2023, January 17\u201321). Smartstate: Detecting state-reverting vulnerabilities in smart contracts via fine-grained state-dependency analysis. Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, Seattle, WA, USA.","DOI":"10.1145\/3597926.3598111"},{"key":"ref_21","unstructured":"Luo, H., Lin, Y., Yan, X., Hu, X., Wang, Y., Zeng, Q., Wang, H., and Jiang, J. (2025). Guiding LLM-based Smart Contract Generation with Finite State Machine. arXiv."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Ladleif, J., and Weske, M. (2019, January 3\u20136). A unifying model of legal smart contracts. Proceedings of the International Conference on Conceptual Modeling, Vienna, Austria.","DOI":"10.1007\/978-3-030-33223-5_27"},{"key":"ref_23","unstructured":"Brenner, M. (2017). Defining the ethereum virtual machine for interactive theorem provers. Financial Cryptography and Data Security, Springer International Publishing."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","article-title":"An overview of the K semantic framework","volume":"79","year":"2010","journal-title":"J. Log. Algebr. Program."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., and Swamy, N. (2016, January 24). Formal verification of smart contracts: Short paper. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, Vienna, Austria.","DOI":"10.1145\/2993600.2993611"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Nehai, Z., Piriou, P.Y., and Daumas, F. (August, January 30). Model-checking of smart contracts. Proceedings of the 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), Halifax, NS, Canada.","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Bai, X., Cheng, Z., Duan, Z., and Hu, K. (2018, January 8\u201310). Formal Modeling and Verification of Smart Contracts. Proceedings of the 2018 7th International Conference on Software and Computer Applications, Kuantan, Malaysia.","DOI":"10.1145\/3185089.3185138"},{"key":"ref_28","unstructured":"Wang, Y., Lahiri, S., Chen, S., Pan, R., Dillig, I., Born, C., Naseer, I., and Ferles, K. (2019). Formal verification of workflow policies for smart contracts in azure blockchain. Verified Software. Theories, Tools, and Experiments, Proceedings of the 11th International Conference, VSTTE 2019, New York, NY, USA, 13\u201314 July 2019, Springer Nature. Revised Selected Papers."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., and Navas, J.A. (2020). solc-verify: A modular verifier for solidity smart contracts. Verified Software. Theories, Tools, and Experiments, Proceedings of the 11th International Conference, VSTTE 2019, New York, NY, USA, 13\u201314 July 2019, Springer. Revised Selected Papers, Volume 12031 of Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-030-41600-3"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., and Ro\u015fu, G. (2018, January 4\u20139). A formal verification tool for ethereum vm bytecode. Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Lake Buena Vista, FL, USA.","DOI":"10.1145\/3236024.3264591"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S., and Dillig, I. (2021, January 24\u201327). SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. Proceedings of the 2021 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA.","DOI":"10.1109\/SP40001.2021.00085"},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"P\u00e9rez-Sol\u00e0, C., Navarro-Arribas, G., Biryukov, A., and Garcia-Alfaro, J. (2019). A minimal core calculus for Solidity contracts. Data Privacy Management, Cryptocurrencies and Blockchain Technology, Springer.","DOI":"10.1007\/978-3-030-31500-9"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Bracciali, A., Clark, J., Pintore, F., R\u00f8nne, P.B., and Sala, M. (2020). Is Solidity solid enough?. Financial Cryptography and Data Security, Springer.","DOI":"10.1007\/978-3-030-43725-1"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Margaria, T., and Steffen, B. (2020). Functional verification of smart contracts via strong data integrity. Leveraging Applications of Formal Methods, Verification and Validation: Applications, Springer.","DOI":"10.1007\/978-3-030-61362-4"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Leucker, M. (2008). Synthesizing monitors for safety properties: This time with calls and returns. International Workshop on Runtime Verification, RV, Springer.","DOI":"10.1007\/978-3-540-89247-2"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Baresi, L., Mehdi, M., Kallehbasti, P., and Rossi, M. (2015, January 16\u201324). Efficient scalable verification of LTL specifications. Proceedings of the ACM\/IEEE International Conference on Software Engineering (ICSE), Florence, Italy.","DOI":"10.1109\/ICSE.2015.84"},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., and Piterman, N. (2016). T2: Temporal property verification. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the TACAS, Eindhoven, The Netherlands, 2\u20138 April 2016, Springer.","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Popeea, C., and Rybalchenko, A. (2013). Solving existentially quantified horn clauses. Computer Aided Verification (CAV), Springer.","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","article-title":"A programming language concept for enhancing software reliability","volume":"SE-12","author":"Strom","year":"1986","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","article-title":"Characterizing finite Kripke structures in propositional temporal logic","volume":"59","author":"Browne","year":"1988","journal-title":"Theor. Comput. Sci."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"1101","DOI":"10.1109\/TR.2018.2876333","article-title":"Verifying full regular temporal properties of programs via dynamic program execution","volume":"68","author":"Wang","year":"2018","journal-title":"IEEE Trans. Reliab."},{"key":"ref_42","unstructured":"Hofmann, M., and Felleisen, M. (2007). Proving that programs eventually do something good. Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Proceedings of the POPL 2007, Nice, France, 17\u201319 January 2007, ACM."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., and Podelski, A. (2015). Fairness modulo theory: A new approach to ltl software model checking. International Conference on Computer Aided Verification, Springer.","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Garfatta, I., Klai, K., Gra\u00efet, M., and Gaaloul, W. (2022, January 25\u201329). Model checking of vulnerabilities in smart contracts: A solidity-to-CPN approach. Proceedings of the 37th ACM\/SIGAPP Symposium on Applied Computing, Brno, Czech Republic.","DOI":"10.1145\/3477314.3507309"},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"185:1","DOI":"10.1145\/3360611","article-title":"Safer smart contract programming with scilla","volume":"3","author":"Sergey","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inf. Comput."},{"key":"ref_47","first-page":"137","article-title":"Automata-theoretic model checking revisited","volume":"Volume 4349","author":"Cook","year":"2007","journal-title":"VMCAI 2007. LNCS"}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/8\/1275\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:26:21Z","timestamp":1760034381000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/8\/1275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,8]]},"references-count":47,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2025,8]]}},"alternative-id":["sym17081275"],"URL":"https:\/\/doi.org\/10.3390\/sym17081275","relation":{},"ISSN":["2073-8994"],"issn-type":[{"value":"2073-8994","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,8]]}}}