{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:26:54Z","timestamp":1777890414683,"version":"3.51.4"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031067723","type":"print"},{"value":"9783031067730","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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_33","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"616-635","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Towards Formal Verification of\u00a0HotStuff-Based Byzantine Fault Tolerant Consensus in\u00a0Agda"],"prefix":"10.1007","author":[{"given":"Harold","family":"Carr","sequence":"first","affiliation":[]},{"given":"Christa","family":"Jenkins","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Moir","sequence":"additional","affiliation":[]},{"given":"Victor Cacciari","family":"Miraldo","sequence":"additional","affiliation":[]},{"given":"Lisandra","family":"Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"33_CR1","unstructured":"King, S., Nadal, S.: PPCoin: peer-to-peer crypto-currency with proof-of-stake (2012). web.archive.org\/web\/20171211072318\/peercoin.net\/assets\/paper\/peercoin-paper.pdf"},{"key":"33_CR2","doi-asserted-by":"publisher","unstructured":"Buterin, V., et al.: Combining GHOST and Casper (2020). https:\/\/doi.org\/10.48550\/ARXIV.2003.03052, arxiv.org\/abs\/2003.03052","DOI":"10.48550\/ARXIV.2003.03052"},{"key":"33_CR3","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (1998). https:\/\/doi.org\/10.1145\/279227.279229","DOI":"10.1145\/279227.279229"},{"key":"33_CR4","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":"33_CR5","unstructured":"Baudet, M., et al.: State machine replication in the Libra blockchain (2019). developers.diem.com\/papers\/diem-consensus-state-machine-replication-in-the-diem-blockchain\/2019-06-28.pdf"},{"key":"33_CR6","unstructured":"The LibraBFT Team: State machine replication in the Libra blockchain, May 2020. developers.diem.com\/papers\/diem-consensus-state-machine-replication-in-the-diem-blockchain\/2020-05-26.pdf"},{"key":"33_CR7","unstructured":"Cachin, C., Vukolic, M.: Blockchain consensus protocols in the wild. CoRR abs\/1707.01873 (2017). arxiv.org\/abs\/1707.01873"},{"key":"33_CR8","doi-asserted-by":"publisher","unstructured":"Tholoniat, P., Gramoli, V.: Formal verification of blockchain byzantine fault tolerance (2019). https:\/\/doi.org\/10.48550\/ARXIV.1909.07453, arxiv.org\/abs\/1909.07453","DOI":"10.48550\/ARXIV.1909.07453"},{"key":"33_CR9","unstructured":"BFT consensus in Agda, December 2021. github.com\/oracle\/bft-consensus-agda\/releases\/tag\/nasafm2022"},{"key":"33_CR10","unstructured":"diem.com: Diem github repository (2021). github.com\/diem\/diem"},{"key":"33_CR11","unstructured":"Carr, H., Jenkins, C., Miraldo, V.C., Moir, M., Silva, L.: An approach to translating Haskell programs to Agda and reasoning about them, March 2022. github.com\/oracle\/bft-consensus-agda\/docs\/README.md"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5"},{"key":"33_CR13","unstructured":"Agda 2.6.1.1 documentation, May 2021. agda.readthedocs.io\/en\/v2.6.1.1"},{"key":"33_CR14","doi-asserted-by":"publisher","unstructured":"Wadler, P., Kokke, W.: Programming language foundations in Agda (2009). https:\/\/doi.org\/10.1016\/j.scico.2020.102440","DOI":"10.1016\/j.scico.2020.102440"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Carr, H., Jenkins, C., Moir, M., Miraldo, V.C., Silva, L.: Towards formal verification of HotStuff-based byzantine fault tolerant consensus in Agda: Extended version (2022). arxiv.org\/abs\/2203.14711","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"33_CR16","doi-asserted-by":"publisher","unstructured":"Spreitzer, M.J., Theimer, M.M., Petersen, K., Demers, A.J., Terry, D.B.: Dealing with server corruption in weakly consistent, replicated data systems. In: Proceedings of the 3rd Annual ACM\/IEEE International Conference on Mobile Computing and Networking, MobiCom 1997, pp. 234\u2013240. ACM, New York (1997). https:\/\/doi.org\/10.1145\/262116.262151","DOI":"10.1145\/262116.262151"},{"key":"33_CR17","volume-title":"Handbook of Applied Cryptography","author":"AJ Menezes","year":"1996","unstructured":"Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press Inc., USA (1996)","edition":"1"},{"key":"33_CR18","unstructured":"Wikipedia: Universe (mathematics), February 2021. en.wikipedia.org\/wiki\/Universe_(mathematics)"},{"key":"33_CR19","unstructured":"Garillot, F., Siles, V.: Librachain, May 2020. github.com\/novifinancial\/LibraChain"},{"key":"33_CR20","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":"33_CR21","doi-asserted-by":"publisher","unstructured":"Kukharenko, V., Ziborov, K., Sadykov, R., Rezin, R.: Verification of HotStuff BFT consensus protocol with TLA+\/TLC in an industrial setting. SHS Web Conf. 93, 01006 (2021). https:\/\/doi.org\/10.1051\/shsconf\/20219301006","DOI":"10.1051\/shsconf\/20219301006"},{"key":"33_CR22","doi-asserted-by":"publisher","unstructured":"Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. Electron. Proc. Theor. Comput. Sci. 310, 50\u201362 (2019). https:\/\/doi.org\/10.4204\/EPTCS.310.6","DOI":"10.4204\/EPTCS.310.6"},{"key":"33_CR23","doi-asserted-by":"publisher","unstructured":"P\u00eerlea, G., Sergey, I.: Mechanising blockchain consensus. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 78\u201390. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3167086","DOI":"10.1145\/3167086"},{"key":"33_CR24","unstructured":"P\u00eerlea, G.: Toychain formally verified blockchain consensus, April 2020. pirlea.net\/papers\/toychain-thesis.pdf"},{"key":"33_CR25","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2009). www.bitcoin.org\/bitcoin.pdf"},{"key":"33_CR26","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer Publishing Company, Incorporated (2010)","edition":"1"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/978-3-319-89884-1_22","volume-title":"Programming Languages and Systems","author":"V Rahli","year":"2018","unstructured":"Rahli, V., Vukotic, I., V\u00f6lp, M., Esteves-Verissimo, P.: Velisarios: byzantine fault-tolerant protocols powered by Coq. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 619\u2013650. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_22"},{"key":"33_CR28","unstructured":"Bickford, M., Constable, R.L., Rahli, V.: Logic of events, a framework to reason about distributed systems. In: 2012 Languages for Distributed Algorithms Workshop, Philadelphia, PA (2012). www.nuprl.org\/documents\/Bickford\/LOE-LADA2012.html"},{"key":"33_CR29","unstructured":"Castro, M., Liskov, B.: Practical byzantine fault tolerance. In: Proceedings of the Third Symposium on Operating Systems Design and Implementation, OSDI 1999, pp. 173\u2013186. USENIX Association, USA (1999)"},{"key":"33_CR30","doi-asserted-by":"publisher","unstructured":"Alturki, M.A., et al.: Towards a verified model of the algorand consensus protocol in Coq. In: Sekerinski, E., et al. (eds.) FM 2019 International Workshops. LNCS, vol. 12232 pp. 362\u2013367 (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_27","DOI":"10.1007\/978-3-030-54994-7_27"},{"key":"33_CR31","doi-asserted-by":"publisher","unstructured":"Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: scaling byzantine agreements for cryptocurrencies. In: Proceedings of the 26th Symposium on Operating Systems Principles, SOSP 2017, pp. 51\u201368. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3132747.3132757","DOI":"10.1145\/3132747.3132757"},{"key":"33_CR32","unstructured":"Crary, K.: Verifying the hashgraph consensus algorithm (2021). arxiv.org\/abs\/2102.01167"},{"key":"33_CR33","unstructured":"Baird, L.: The Swirlds hashgraph consensus algorithm: fair, fast, byzantine fault tolerance. Technical report SWIRLDS-TR-2016-01 (2016). www.swirlds.com\/downloads\/SWIRLDS-TR-2016-01.pdf"},{"key":"33_CR34","unstructured":"Losa, G., Dodds, M.: On the formal verification of the Stellar consensus protocol. In: 2nd Workshop on Formal Methods for Blockchains (2020). drops.dagstuhl.de\/opus\/volltexte\/2020\/13422\/pdf\/OASIcs-FMBC-2020-9.pdf"},{"key":"33_CR35","unstructured":"Alturki, M.A., et al.: Verifying Gasper with dynamic validator sets in Coq (2020). github.com\/runtimeverification\/beacon-chain-verification\/blob\/master\/casper\/report\/report.pdf"},{"key":"33_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-030-03424-5_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems","author":"I Konnov","year":"2018","unstructured":"Konnov, I., Widder, J.: ByMC: byzantine model checker. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018, Part III. LNCS, vol. 11246, pp. 327\u2013342. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_22"},{"key":"33_CR37","doi-asserted-by":"publisher","unstructured":"Crain, T., Gramoli, V., Larrea, M., Raynal, M.: DBFT: efficient leaderless byzantine consensus and its application to blockchains. In: 2018 IEEE 17th International Symposium on Network Computing and Applications (NCA), pp. 1\u20138 (2018). https:\/\/doi.org\/10.1109\/NCA.2018.8548057","DOI":"10.1109\/NCA.2018.8548057"},{"key":"33_CR38","unstructured":"Braithwaite, S., et al.: Formal specification and model checking of the Tendermint blockchain synchronization protocol. In: 2nd Workshop on Formal Methods for Blockchains (2020). drops.dagstuhl.de\/opus\/volltexte\/2020\/13423\/pdf\/OASIcs-FMBC-2020-10.pdf"},{"key":"33_CR39","doi-asserted-by":"publisher","unstructured":"Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on BFT consensus (2018). https:\/\/doi.org\/10.48550\/ARXIV.1807.04938, arxiv.org\/abs\/1807.04938","DOI":"10.48550\/ARXIV.1807.04938"},{"key":"33_CR40","doi-asserted-by":"publisher","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","DOI":"10.1145\/42282.42283"},{"key":"33_CR41","unstructured":"Buterin, V., Griffith, V.: Casper the friendly finality gadget. CoRR abs\/1710.09437 (2017). arxiv.org\/abs\/1710.09437"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T11:13:25Z","timestamp":1659352405000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_33","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":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","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":"118","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":"33","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":"6","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":"28% - 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":"6.3","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}