{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T06:45:52Z","timestamp":1774853152053,"version":"3.50.1"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032123343","type":"print"},{"value":"9783032123350","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-12335-0_1","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:12:32Z","timestamp":1768201952000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Automating Blockchain Consensus Verification with\u00a0IsabeLLM"],"prefix":"10.1007","author":[{"given":"Elliot","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"Knottenbelt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"1_CR1","unstructured":"Alchemy: What are upgradeable smart contracts? (2024). https:\/\/docs.alchemy.com\/docs\/upgradeable-smart-contracts. Accessed Apr 2025"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alhabardi, F., Setzer, A.: A simulator of Solidity-style smart contracts in the theorem prover Agda. In: Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications, pp. 1\u201311 (2023)","DOI":"10.1145\/3651655.3651656"},{"key":"1_CR3","unstructured":"Alhabardi, F.F., Beckmann, A., Lazar, B., Setzer, A.: Verification of bitcoin script in Agda using weakest preconditions for access control. arXiv preprint arXiv:2203.03054 (2022)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Alturki, M.A., et al.: Towards a verified model of the Algorand consensus protocol in coq. In: International Symposium on Formal Methods, pp. 362\u2013367. Springer (2019)","DOI":"10.1007\/978-3-030-54994-7_27"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 66\u201377 (2018)","DOI":"10.1145\/3167084"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Chiang, J.H.y., Lafuente, A.L.: Towards a theory of decentralized finance. In: Financial Cryptography and Data Security. FC 2021 International Workshops: CoDecFin, DeFi, VOTING, and WTSC, Virtual Event, March 5, 2021, Revised Selected Papers 25, pp. 227\u2013232. Springer (2021)","DOI":"10.1007\/978-3-662-63958-0_20"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Chiang, J.H.y., Lluch-Lafuente, A.: A theory of automated market makers in DeFi. Logical Methods Comput. Sci. 18 (2022)","DOI":"10.46298\/lmcs-18(4:12)2022"},{"key":"1_CR8","unstructured":"Bartoletti, M., Zunino, R.: A theoretical basis for blockchain extractable value. arXiv preprint arXiv:2302.02154 (2023)"},{"key":"1_CR9","unstructured":"Blockchain.com: BTC total number of transactions (2025). https:\/\/www.blockchain.com\/explorer\/charts\/n-transactions-total. Accessed Apr 2025"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/3591335.3591343","volume":"42","author":"T Bordis","year":"2023","unstructured":"Bordis, T., Runge, T., Kittelmann, A., Schaefer, I.: Correctness-by-construction: an overview of the corc ecosystem. Ada Lett. 42(2), 75\u201378 (2023)","journal-title":"Ada Lett."},{"key":"1_CR11","unstructured":"Certora: Certora prover. https:\/\/www.certora.com\/prover"},{"key":"1_CR12","unstructured":"Chainalysis: The \\$80 million qubit hack likely the work of north Korea-linked cybercriminals (2023). https:\/\/www.chainalysis.com\/blog\/qubit-hack-north-korea\/. Accessed Apr 2025"},{"key":"1_CR13","unstructured":"CoinBase: Ethereum classic and the Ethereum hard fork (2016). https:\/\/help.coinbase.com\/en\/coinbase\/getting-started\/crypto-education\/eth-hard-fork. Accessed Apr 2025"},{"key":"1_CR14","unstructured":"CoinDesk: The Vertcoin cryptocurrency just got 51% attacked\u00a0\u2013 again (2019). https:\/\/www.coindesk.com\/tech\/2019\/12\/02\/the-vertcoin-cryptocurrency-just-got-51-attacked-again. Accessed Apr 2025"},{"key":"1_CR15","unstructured":"CoinDesk: Bad actors rent hashing power to hit bitcoin gold with new 51% attacks (2020), https:\/\/www.coindesk.com\/tech\/2020\/01\/27\/bad-actors-rent-hashing-power-to-hit-bitcoin-gold-with-new-51-attacks. Accessed Apr 2025"},{"key":"1_CR16","unstructured":"CoinDesk: Ethereum classic hit by third 51% attack in a month (2021). https:\/\/www.coindesk.com\/markets\/2020\/08\/29\/ethereum-classic-hit-by-third-51-attack-in-a-month. Accessed Apr 2025"},{"key":"1_CR17","unstructured":"CoinMarketCap: BTC market capitalisation (2025). https:\/\/coinmarketcap.com\/currencies\/bitcoin\/. Accessed Apr 2025"},{"key":"1_CR18","unstructured":"Consensys: Mythril. https:\/\/mythx.io\/"},{"key":"1_CR19","unstructured":"Decrypt: BNB chain hits record-high sandwich attacks exposing \\$1.5 billion in trades (2024). https:\/\/decrypt.co\/294648\/bnb-smart-chain-blocks-hits-record-high-sandwich-attacks. Accessed Apr 2025"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Foster, S., Huerta\u00a0y Munive, J.J., Gleirscher, M., Struth, G.: Hybrid systems verification with Isabelle\/HOL: Simpler syntax, better models, faster proofs. In: Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20\u201326, 2021, Proceedings 24, pp. 367\u2013386. Springer (2021)","DOI":"10.1007\/978-3-030-90870-6_20"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol: analysis and applications. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp. 281\u2013310. Springer (2015)","DOI":"10.1007\/978-3-662-46803-6_10"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Gomes, V.B., Kleppmann, M., Mulligan, D.P., Beresford, A.R.: Verifying strong eventual consistency in distributed systems. Proc. ACM Programm. Lang. 1(OOPSLA), 1\u201328 (2017)","DOI":"10.1145\/3133933"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et\u00a0al.: Kevm: A complete formal semantics of the Ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 204\u2013217. IEEE (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from isabelle\/HOL to CakeML. In: European Symposium on Programming, pp. 999\u20131026. Springer (2018)","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"1_CR25","unstructured":"Investopedia: Crypto worth over \\$320 million taken in wormhole hack (2022). https:\/\/www.investopedia.com\/crypto-theft-of-usd320-million-wormhole-hack-5218062. Accessed Apr 2025"},{"key":"1_CR26","unstructured":"Investopedia: What are smart contracts on the blockchain and how do they work? (2024). https:\/\/www.investopedia.com\/terms\/s\/smart-contracts.asp#:~:text=Smart%20Contract%20Pros%20and%20Cons&text=Accuracy%3A%20There%20can%20be%20no,The%20programming%20cannot%20be%20altered. Accessed Apr 2025"},{"key":"1_CR27","unstructured":"Isabelle\/HOL: Archive of formal proofs (2004), https:\/\/www.isa-afp.org\/, [Accessed April 2025]"},{"key":"1_CR28","unstructured":"Jiang, A.Q., Li, W., Han, J.M., Wu, Y.: Lisa: Language models of isabelle proofs. In: 6th Conference on Artificial Intelligence and Theorem Proving (AITP) (2021)"},{"key":"1_CR29","unstructured":"Jones, E.: IsabeLLM. https:\/\/github.com\/EllbellCode\/IsabeLLM (2025)"},{"key":"1_CR30","unstructured":"Jones, E., Marmsoler, D.: Towards mechanised consensus in isabelle. In: 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Klein, G., Sewell, T., Winwood, S.: Refinement in the formal verification of the seL4 microkernel. In: Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323\u2013339. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9_11"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Leite, G., Arruda, F., Antonino, P., Sampaio, A., Roscoe, A.: Extracting formal smart-contract specifications from natural language with LLMs. In: International Conference on Formal Aspects of Component Software, pp. 109\u2013126. Springer (2024)","DOI":"10.1007\/978-3-031-71261-6_7"},{"key":"1_CR33","unstructured":"Li, W., Yu, L., Wu, Y., Paulson, L.C.: Isarstep: a benchmark for high-level mathematical reasoning. arXiv preprint arXiv:2006.09265 (2020)"},{"key":"1_CR34","unstructured":"Lin, X., et al.: FVEL: Interactive formal verification environment with large language models via theorem proving (2024). https:\/\/arxiv.org\/abs\/2406.14408"},{"issue":"50","key":"1_CR35","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theoret. Comput. Sci. 411(50), 4333\u20134356 (2010)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Marmsoler, D., Brucker, A.D.: A denotational semantics of solidity in Isabelle\/HOL. In: International Conference on Software Engineering and Formal Methods, pp. 403\u2013422. Springer (2021)","DOI":"10.1007\/978-3-030-92124-8_23"},{"key":"1_CR37","unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system. Decentralized business review (2008)"},{"key":"1_CR38","unstructured":"Nethermind: Clear\u2013prove anything about your Solidity smart contracts (2024). https:\/\/www.nethermind.io\/blog\/clear-prove-anything-about-your-solidity-smart-contracts"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"1_CR40","unstructured":"Paulson, L.C.: Theory ramsey (2004). https:\/\/isabelle.in.tum.de\/website-Isabelle2021-1\/dist\/library\/HOL\/HOL-Library\/Ramsey.html"},{"key":"1_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","volume":"55","author":"LC Paulson","year":"2015","unstructured":"Paulson, L.C.: A mechanised proof of g\u00f6del\u2019s incompleteness theorems using Nominal Isabelle. J. Autom. Reason. 55, 1\u201337 (2015)","journal-title":"J. Autom. Reason."},{"key":"1_CR42","unstructured":"Pusceddu, D., Bartoletti, M.: Formalizing automated market makers in the Lean 4 theorem prover. arXiv preprint arXiv:2402.06064 (2024)"},{"key":"1_CR43","unstructured":"Reuters: How hackers stole \\$613 million in crypto tokens from poly network (2021). https:\/\/www.reuters.com\/technology\/how-hackers-stole-613-million-crypto-tokens-poly-network-2021-08-12\/. Accessed Apr 2025"},{"key":"1_CR44","unstructured":"Setzer, A.: Modelling bitcoin in Agda. arXiv preprint arXiv:1804.06398 (2018)"},{"issue":"2","key":"1_CR45","doi-asserted-by":"publisher","first-page":"255","DOI":"10.3390\/electronics9020255","volume":"9","author":"T Sun","year":"2020","unstructured":"Sun, T., Yu, W.: A formal verification framework for security issues of blockchain smart contracts. Electronics 9(2), 255 (2020)","journal-title":"Electronics"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 88\u201399 (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"1_CR47","unstructured":"Unruh, D.: scala-isabelle\u00a0\u2013 a scala library for controlling isabelle\/hol (2022). https:\/\/dominique-unruh.github.io\/scala-isabelle\/. Accessed Apr 2025"},{"key":"1_CR48","unstructured":"Wang, H., et\u00a0al.: Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656 (2023)"},{"key":"1_CR49","unstructured":"Xin, H., et al.: Deepseek-prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333 (2024)"},{"key":"1_CR50","unstructured":"Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: International Conference on Machine Learning, pp. 6984\u20136994. PMLR (2019)"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Yang, K., et al.: Leandojo: theorem proving with retrieval-augmented language models. Adv. Neural. Inf. Process. Syst. 36, 21573\u201321612 (2023)","DOI":"10.52202\/075280-0944"},{"key":"1_CR52","doi-asserted-by":"publisher","first-page":"21411","DOI":"10.1109\/ACCESS.2020.2969437","volume":"8","author":"Z Yang","year":"2020","unstructured":"Yang, Z., Lei, H., Qian, W.: A hybrid formal verification system in coq for ensuring the reliability and security of Ethereum-based service smart contracts. IEEE Access 8, 21411\u201321436 (2020)","journal-title":"IEEE Access"}],"container-title":["Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","Blockchain Technology and Emerging Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-12335-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T05:23:04Z","timestamp":1774848184000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-12335-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032123343","9783032123350"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-12335-0_1","relation":{},"ISSN":["1867-8211","1867-822X"],"issn-type":[{"value":"1867-8211","type":"print"},{"value":"1867-822X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Blocktea","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Blockchain Technology and Emerging Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Venice","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"blocktea2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/blocktea.eai-conferences.org\/2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}