{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:16:15Z","timestamp":1783545375209,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Many compilation stages of smart contracts on the Ethereum blockchain have been transitioned to the intermediate language . Tasks such as smart contract optimization and bytecode generation are\u2014or will soon be\u2014performed directly at the  level in the compilers for the higher-level languages such as Solidity. In this paper, we develop a formal semantics of  programs in Rocq, suitable for verification, which allows formal reasoning at the level of  code or generation tools processing  programs. Our semantics is\n                    <jats:italic>expressive<\/jats:italic>\n                    enough to be the basis for formal verification tools, and\n                    <jats:italic>simple<\/jats:italic>\n                    enough to make the development of such tools feasible. In order to prove its adequacy for verification, we develop in Rocq a checker (and associated soundness proofs), based on our semantics, able to verify the results of the liveness analysis stage of the official Solidity compiler , which opens the door towards formally verified Ethereum\u2019s smart contracts compilation. Experiments on more than 1,500 smart contracts show that we are able to automatically verify \u2019s liveness analysis results in negligible time.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_13","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:22:30Z","timestamp":1779024150000},"page":"255-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Formally Verified Smart Contracts Compilation"],"prefix":"10.1007","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrique","family":"Martin-Martin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"13_CR1","unstructured":"FE: The next generation smart contract language for Ethereum. https:\/\/fe-lang.org"},{"key":"13_CR2","unstructured":"A formal verification tool for Solidity smart contracts by Nethermind Security. https:\/\/github.com\/NethermindEth\/Clear. Accessed 27 Nov 2025"},{"key":"13_CR3","unstructured":"The solc optimizer (2021). https:\/\/docs.soliditylang.org\/en\/v0.8.7\/internals\/optimizer.html"},{"key":"13_CR4","unstructured":"FORVES: Formally Verified EVM Block-Optimizations (2024). https:\/\/github.com\/costa-group\/forves. Accessed 27 Nov 2025"},{"key":"13_CR5","unstructured":"coq-of-solidity (2025). https:\/\/github.com\/formal-land\/coq-of-solidity. Accessed 27 Nov 2025"},{"key":"13_CR6","unstructured":"FORYU: A Formal Semantics for Yul in Coq (2025). https:\/\/github.com\/costa-group\/foryu. Accessed 27 Nov 2025"},{"key":"13_CR7","unstructured":"Semantic tests of solidity (2025). https:\/\/github.com\/argotorg\/solidity\/tree\/develop\/test\/libsolidity\/semanticTests. Accessed 27 Nov 2025"},{"key":"13_CR8","unstructured":"Solidity documentation (2025). https:\/\/docs.soliditylang.org\/en\/latest\/index.html"},{"key":"13_CR9","unstructured":"Yul (2025). https:\/\/docs.soliditylang.org\/en\/latest\/yul.html. Accessed 27 Nov 2025"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Albert, E., Genaim, S., Martin-Martin, E.: Towards Formally Verified Smart Contracts Compilation (FM\u201926 Artifact) (2026). https:\/\/doi.org\/10.5281\/zenodo.18612372. Accessed 13 Feb 2026","DOI":"10.5281\/zenodo.18612372"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: CPP, pp. 66\u201377. ACM (2018)","DOI":"10.1145\/3167084"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Barri\u00e8re, A., Blazy, S., Fl\u00fcckiger, O., Pichardie, D., Vitek, J.: Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5(POPL), 1\u201326 (2021)","DOI":"10.1145\/3434327"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-28869-2_3","volume-title":"Programming Languages and Systems","author":"G Barthe","year":"2012","unstructured":"Barthe, G., Demange, D., Pichardie, D.: A formally verified SSA-Based Middle-End. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 47\u201366. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_3"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development - Coq\u2019Art: the calculus of inductive constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Cassez, F., Fuller, J., Asgaonkar, A.: Formal verification of the ethereum 2.0 beacon chain. In: Fisman, D., Rosu, G., (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings, Part I, vol. 13243 of Lecture Notes in Computer Science, pp. 167\u2013182. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_9"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Demange, D., Pichardie, D., Stefanesco, L.: Verifying fast and sparse SSA-based optimizations in Coq. In: Franke, B., (ed.), Compiler Construction - 24th International Conference, CC 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, vol. 9031 of Lecture Notes in Computer Science, pp. 233\u2013252. Springer (2015)","DOI":"10.1007\/978-3-662-46663-6_12"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Dill, D.L., et al.: Fast and reliable formal verification of smart contracts with the move prover. In: Fisman, D., Rosu, G., (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, vol. 13243 of Lecture Notes in Computer Science, pp. 183\u2013200. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_10"},{"key":"13_CR18","unstructured":"Ethereum. Vyper (2024). https:\/\/vyper.readthedocs.io. Accessed 27 Nov 2025"},{"issue":"OOPSLA2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"2402","DOI":"10.1145\/3689796","volume":"8","author":"S Grossman","year":"2024","unstructured":"Grossman, S., et al.: Practical verification of smart contracts using memory splitting. Proc. ACM Program. Lang. 8(OOPSLA2), 2402\u20132433 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al., (eds.) Financial Cryptography and Data Security, pp. 520\u2013535. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"13_CR21","unstructured":"INRIA. The Rocq Reference Manual - Version 9.1.0 (2025). https:\/\/rocq-prover.org\/doc\/V9.1.0\/refman\/index.html"},{"key":"13_CR22","unstructured":"ivan71kmayshan27. Coq formalisation of the ethereum virtual machine (wip) (2020). https:\/\/github.com\/ivan71kmayshan27\/coq-evm. Accessed 23 June 2022"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Lin, Y., Tzevelekos, N.: An operational semantics for YUL. In: Madeira, A., Knapp, A., (eds.) Software Engineering and Formal Methods - 22nd International Conference, SEFM 2024, Aveiro, Portugal, November 6-8, 2024, Proceedings, vol. 15280 of Lecture Notes in Computer Science, pp. 328\u2013346. Springer (2024)","DOI":"10.1007\/978-3-031-77382-2_19"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-030-51054-1_19","volume-title":"Automated Reasoning","author":"J-C L\u00e9chenet","year":"2020","unstructured":"L\u00e9chenet, J.-C., Blazy, S., Pichardie, D.: A fast verified liveness analysis in SSA form. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 324\u2013340. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_19"},{"issue":"7","key":"13_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"7","key":"13_CR26","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"13_CR27","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10009-024-00760-3","volume":"26","author":"D Monniaux","year":"2024","unstructured":"Monniaux, D.: Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilers. Int. J. Softw. Tools Technol. Transf. 26(4), 463\u2013477 (2024)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Monniaux, D., Six, C.: Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. In: Henkel, J., Liu, X., (eds.) LCTES \u201921: 22nd ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021, pp. 85\u201396. ACM (2021)","DOI":"10.1145\/3461648.3463850"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Schneidewind, C., Grishchenko, I., Scherer, M., Maffei, M.: Ethor: practical and provably sound static analysis of Ethereum smart contracts. In: CCS \u201920: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, 9\u201313 November 2020, pp. 621\u2013640. ACM (2020)","DOI":"10.1145\/3372297.3417250"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Six, C., Boulm\u00e9, S., Monniaux, D.: Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang. 4(OOPSLA), 129:1\u2013129:29 (2020)","DOI":"10.1145\/3428197"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Six, C., et al.: Formally verified superblock scheduling. In: Popescu, A., Zdancewic, S., (eds.) CPP \u201922: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 \u2013 18, 2022, pp. 40\u201354. ACM (2022)","DOI":"10.1145\/3497775.3503679"},{"key":"13_CR34","unstructured":"Stegeman, L., Solitor: runtime verification of smart contracts on the Ethereum network. Master\u2019s thesis, University of Twente (2018)"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Tristan, J., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Necula, G.C. Wadler, P., (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008, pp. 17\u201327. ACM (2008)","DOI":"10.1145\/1328438.1328444"},{"key":"13_CR36","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (Berlin version 8fea825 \u2013 2022-08-22) (2022)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:45Z","timestamp":1783542645000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}