{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:57:01Z","timestamp":1781132221765,"version":"3.54.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032281869","type":"print"},{"value":"9783032281876","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-28187-6_6","type":"book-chapter","created":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:03:41Z","timestamp":1781129021000},"page":"93-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling of\u00a0Beefy, a\u00a0Protocol for\u00a0Supporting Light Clients"],"prefix":"10.1007","author":[{"given":"Daniel O.","family":"Dirdal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leander","family":"Jehl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bhargav Nagaraj","family":"Bhatt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hein","family":"Meling","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nejm","family":"Saadallah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,11]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881","DOI":"10.1017\/CBO9781139195881"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-031-93706-4_9","volume-title":"NASA Formal Methods","author":"N Bertrand","year":"2025","unstructured":"Bertrand, N., Ghorpade, P., Rubin, S., Scholz, B., Suboti\u0107, P.: Reusable formal verification of DAG-based consensus protocols. In: Dutle, A., Humphrey, L., Titolo, L. (eds.) NFM 2025. LNCS, vol. 15682, pp. 138\u2013158. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_9"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Bhatt, B.N., Shirazi, F., Stewart, A.: Trustless bridges via random sampling light clients. In: Avarikioti, Z., Christin, N. (eds.) 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0354, pp. 31:1\u201331:24. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.AFT.2025.31","DOI":"10.4230\/LIPIcs.AFT.2025.31"},{"key":"6_CR4","unstructured":"Boneh, D., Drijvers, M., Neven, G.: Compact multi-signatures for smaller blockchains. Cryptology ePrint Archive, Paper 2018\/483 (2018). https:\/\/eprint.iacr.org\/2018\/483"},{"key":"6_CR5","unstructured":"Braithwaite, S., et al.: A tendermint light client (2020). https:\/\/arxiv.org\/abs\/2010.07031"},{"key":"6_CR6","unstructured":"Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on BFT consensus (2019). https:\/\/arxiv.org\/abs\/1807.04938"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Bunz, B., Kiffer, L., Luu, L., Zamani, M.: FlyClient: super-light clients for cryptocurrencies. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, 18\u201321 May 2020. pp. 928\u2013946. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00049","DOI":"10.1109\/SP40000.2020.00049"},{"key":"6_CR8","unstructured":"Burdges, J., et al.: Overview of polkadot and its design considerations (2020). https:\/\/arxiv.org\/abs\/2005.13456"},{"key":"6_CR9","unstructured":"Buterin, V.: A next-generation smart contract and decentralized application platform. Whitepaper (2014). https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"key":"6_CR10","unstructured":"Buterin, V., Griffith, V.: Casper the friendly finality gadget (2019). https:\/\/arxiv.org\/abs\/1710.09437"},{"key":"6_CR11","unstructured":"Chaidos, P., et al.: Crossing with confidence: Formal analysis and model checking of blockchain bridges. Cryptology ePrint Archive, Paper 2026\/292 (2026). https:\/\/eprint.iacr.org\/2026\/292"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Chatzigiannis, P., Baldimtsi, F., Chalkias, K.: SoK: blockchain light clients. In: Eyal, I., Garay, J. (eds.) FC 2022. LNCS, vol. 13411. pp. 615\u2013641. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-18283-9_31","DOI":"10.1007\/978-3-031-18283-9_31"},{"key":"6_CR13","unstructured":"DefiLlama: Hacks (2025). https:\/\/defillama.com\/hacks. Accessed 18 Nov 2025"},{"key":"6_CR14","unstructured":"Dirdal, D.O.: Formal specification of BEEFY (2025). https:\/\/github.com\/relab\/formal-modeling-beefy-artifacts"},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288\u2013323 (1988). https:\/\/doi.org\/10.1145\/42282.42283","journal-title":"J. ACM"},{"key":"6_CR16","unstructured":"Foundation, E., Contributors, C.S.: Ethereum consensus specification: altair light client sync protocol (2024). https:\/\/ethereum.github.io\/consensus-specs\/specs\/altair\/light-client\/sync-protocol\/"},{"key":"6_CR17","unstructured":"Foundation, W.: Finality. https:\/\/spec.polkadot.network\/sect-finality"},{"key":"6_CR18","unstructured":"Informal Systems: Quint: The quint specification language (2026). https:\/\/quint-lang.org\/"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-78089-0_13","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Jehl","year":"2021","unstructured":"Jehl, L.: Formal verification of HotStuff. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 197\u2013204. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_13"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360549","DOI":"10.1145\/3360549"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kuppe, M., Merz, S.: Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 88\u2013105. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_6","DOI":"10.1007\/978-3-031-19849-6_6"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"6_CR23","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA (2002)"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4, 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Llamb\u00edas, G., Gonz\u00e1lez, L., Ruggia, R.: Formalising a gateway-based blockchain interoperability solution with event-B. In: 2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), pp. 1\u20139. (2024). https:\/\/doi.org\/10.1109\/ICBC59979.2024.10634427","DOI":"10.1109\/ICBC59979.2024.10634427"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Mari\u0107, F., Scholz, B., Suboti\u0107, P.: Formal verification of a fail-safe cross-chain bridge. In: Marmsoler, D., Xu, M. (eds.) 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), vol.\u00a0129, pp. 8:1\u20138:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2025). https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2025.8","DOI":"10.4230\/OASIcs.FMBC.2025.8"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Neha\u00ef, Z., Bobot, F., Tucci-Piergiovanni, S., Delporte-Gallet, C., Fauconnier, H.: A TLA+ formal proof of a cross-chain swap. In: Proceedings of the 23rd International Conference on Distributed Computing and Networking., ICDCN 2022, pp. 148\u2013159. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3491003.3491006","DOI":"10.1145\/3491003.3491006"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol.\u00a02283. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR29","unstructured":"ParityTech: Polkadot SDK. https:\/\/github.com\/paritytech\/polkadot-sdk"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-981-99-7584-6_15","volume-title":"Formal Methods and Software Engineering","author":"B Pillai","year":"2023","unstructured":"Pillai, B., H\u00f3u, Z., Biswas, K., Muthukkumarasamy, V.: Formal verification of the burn-to-claim blockchain interoperable protocol. In: Li, Y., Tahar, S. (eds.) ICFEM 2023. LNCS, vol. 14308, pp. 249\u2013254. Springer Nature Singapore, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-99-7584-6_15"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Qiu, L., Kim, Y., Shin, J.Y., Kim, J., Honor\u00e9, W., Shao, Z.: Lido: linearizable byzantine distributed objects with refinement-based liveness proofs. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656423","DOI":"10.1145\/3656423"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Qiu, L., Xiao, J., Shin, J.Y., Shao, Z.: Lido-DAG: a framework for verifying safety and liveness of DAG-based consensus protocols. Proc. ACM Program. Lang. 9(PLDI) (2025). https:\/\/doi.org\/10.1145\/3729306","DOI":"10.1145\/3729306"},{"key":"6_CR33","unstructured":"Stewart, A., Kokoris-Kogia, E.: Grandpa: a byzantine finality gadget (2020). https:\/\/arxiv.org\/abs\/2007.01560"},{"key":"6_CR34","unstructured":"Team, S.: Snowbridge (2025). https:\/\/docs.snowbridge.network\/. Accessed 18 Nov 2025"},{"key":"6_CR35","unstructured":"Team, T.: Tendermint specifications (2020). https:\/\/github.com\/tendermint\/tendermint\/tree\/master\/spec"},{"key":"6_CR36","unstructured":"Technologies, P.: Beefy (2025). https:\/\/github.com\/paritytech\/polkadot-sdk\/tree\/master\/substrate\/client\/consensus\/beefy"},{"key":"6_CR37","unstructured":"Todd, P.: Making UTXO set growth irrelevant with low-latency delayed TXO commitments (2016). https:\/\/lists.linuxfoundation.org\/pipermail\/bitcoin-dev\/2016-May\/012715.html"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Wei, Q., Zhao, X., Zhu, X.Y., Zhang, W.: Formal analysis of IBC protocol. In: 2023 IEEE 31st International Conference on Network Protocols (ICNP) (2023). https:\/\/doi.org\/10.1109\/ICNP59649.2023.10355573","DOI":"10.1109\/ICNP59649.2023.10355573"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Yin, M., Malkhi, D., Reiter, M.K., Gueta, G.G., Abraham, I.: HotStuff: BFT consensus with linearity and responsiveness. In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, pp. 347\u2013356. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3293611.3331591","DOI":"10.1145\/3293611.3331591"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28187-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:03:45Z","timestamp":1781129025000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28187-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032281869","9783032281876"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28187-6_6","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":"11 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Urbino","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"46","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2026\/forte","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}