{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:37Z","timestamp":1779074737051,"version":"3.51.4"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the <jats:italic>validators<\/jats:italic>, their <jats:italic>stakes<\/jats:italic>, their <jats:italic>attestations<\/jats:italic> (votes) and if some validators are found to be dishonest, to <jats:italic>slash<\/jats:italic> them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The <jats:italic>Beacon Chain reference implementation<\/jats:italic> developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain\u2019s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed <jats:italic>verified<\/jats:italic> fixes. We have also synthesised <jats:italic>functional correctness specifications<\/jats:italic> that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/ConsenSys\/eth2.0-dafny\">https:\/\/github.com\/ConsenSys\/eth2.0-dafny<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_9","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"167-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Formal Verification of the Ethereum 2.0 Beacon Chain"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4317-5025","authenticated-orcid":false,"given":"Franck","family":"Cassez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joanne","family":"Fuller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aditya","family":"Asgaonkar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"9_CR1","unstructured":"Alturki, M., Bogdanas, D., Hathhorn, C., Park, D., Ro\u015fu, G.: An executable K model of ethereum 2.0 beacon chain phase 0 specification. Project Report (2020), https:\/\/github.com\/runtimeverification\/beacon-chain-spec"},{"key":"9_CR2","unstructured":"Buterin, V., Hernandez, D., Kamphefner, T., Pham, K., Qiao, Z., Ryan, D., Sin, J., Wang, Y., Zhang, Y.X.: Combining GHOST and casper. CoRR abs\/2003.03052 (2020), https:\/\/arxiv.org\/abs\/2003.03052"},{"key":"9_CR3","unstructured":"ConsenSys: Formal verification of the ethereum 2.0 specifications in dafny. (2021), https:\/\/github.com\/ConsenSys\/eth2.0-dafny"},{"key":"9_CR4","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)"},{"key":"9_CR5","unstructured":"Edgington, B.: (2020), https:\/\/benjaminion.xyz\/eth2-annotated-spec\/"},{"key":"9_CR6","unstructured":"Ethereum Foundation: Beacon chain specifications (2020), https:\/\/github.com\/ethereum\/consensus-specs\/blob\/dev\/specs\/phase0\/beacon-chain.md"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07792, pp. 125\u2013128. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8,","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4) (Oct 2009). https:\/\/doi.org\/10.1145\/1592434.1592438,","DOI":"10.1145\/1592434.1592438"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563,","DOI":"10.1145\/359545.359563"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212,","DOI":"10.1109\/MS.2017.4121212"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Li, E., Serbanuta, T., Diaconescu, D., Zamfir, V., Rosu, G.: Formalizing correct-by-construction casper in coq. In: IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020, Toronto, ON, Canada, May 2-6, 2020. pp.\u00a01\u20133. IEEE (2020). https:\/\/doi.org\/10.1109\/ICBC48266.2020.9169468,","DOI":"10.1109\/ICBC48266.2020.9169468"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a050, pp. 104\u2013125. IOS Press (2017). https:\/\/doi.org\/10.3233\/978-1-61499-810-5-104,","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer Publishing Company, Incorporated (2014)","DOI":"10.1007\/978-3-319-10542-0"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures. Lecture Notes in Computer Science, vol. 11430, pp. 1\u201337. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-17601-3_1,","DOI":"10.1007\/978-3-030-17601-3_1"},{"key":"9_CR15","unstructured":"Ryan, D.: (2020), https:\/\/notes.ethereum.org\/@djrtwo\/Bkn3zpwxB#Phase-0-for-Humans-v0100"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:20:57Z","timestamp":1648534857000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}