{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,2]],"date-time":"2026-09-02T21:22:37Z","timestamp":1788384157079,"version":"build-2803163510"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032008275","type":"print"},{"value":"9783032008282","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"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-00828-2_21","type":"book-chapter","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T16:23:29Z","timestamp":1760631809000},"page":"379-400","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Nondeterministic Behaviours in\u00a0the\u00a0Tendermint Byzantine Fault Tolerant Blockchain Consensus Protocol"],"prefix":"10.1007","author":[{"given":"Yisong","family":"Yu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naipeng","family":"Dong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,17]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1016\/j.comcom.2022.06.014","volume":"192","author":"H Afzaal","year":"2022","unstructured":"Afzaal, H., Imran, M., Janjua, M.U.: Formal verification of persistence and liveness in the trust-based blockchain crowdsourcing consensus protocol. Comput. Commun. 192, 384\u2013401 (2022)","journal-title":"Comput. Commun."},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"55077","DOI":"10.1109\/ACCESS.2024.3389551","volume":"12","author":"H Afzaal","year":"2024","unstructured":"Afzaal, H., Zafar, N.A., Tehseen, A., Kousar, S., Imran, M.: Formal verification of justification and finalization in beacon chain. IEEE Access 12, 55077\u201355102 (2024)","journal-title":"IEEE Access"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-030-54994-7_27","volume-title":"Formal Methods. FM 2019 International Workshops","author":"MA Alturki","year":"2020","unstructured":"Alturki, M.A., Chen, J., Luchangco, V., Moore, B., Palmskog, K., Pe\u00f1a, L., Ro\u015fu, G.: Towards a verified model of the algorand consensus protocol in coq. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 362\u2013367. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_27"},{"key":"21_CR4","unstructured":"Amoussou-Guenou, Y., Pozzo, A.D., Potop-Butucaru, M., Tucci-Piergiovanni, S.: Correctness and fairness of tendermint-core blockchains (2018). https:\/\/arxiv.org\/abs\/1805.08429"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Baloochestani, A., Jehl, L.: Eiffel: Extending formal verification of distributed algorithms to utility analysis. In: 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS), pp.\u00a01\u20137 (2023)","DOI":"10.1109\/BRAINS59668.2023.10316928"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-030-25543-5_15","volume-title":"Computer Aided Verification","author":"I Berkovits","year":"2019","unstructured":"Berkovits, I., Lazi\u0107, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 245\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/978-3-030-61362-4_27","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"S Braithwaite","year":"2020","unstructured":"Braithwaite, S., Buchman, E., Konnov, I., Milosevic, Z., Stoilkovska, I., Widder, J., Zamfir, A.: Tendermint blockchain synchronization: formal specification and model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 471\u2013488. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_27"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1","volume-title":"Automated Reasoning","year":"2020","unstructured":"Peltier, N., Sofronie-Stokkermans, V. (eds.): IJCAR 2020. LNCS (LNAI), vol. 12167. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1"},{"key":"21_CR9","unstructured":"Buchman, E.: Tendermint: byzantine fault tolerance in the age of blockchains (2016). https:\/\/api.semanticscholar.org\/CorpusID:59082906"},{"key":"21_CR10","unstructured":"Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on BFT consensus. CoRR arxiv:1807.04938 (2018)"},{"key":"21_CR11","unstructured":"Castro, M., Liskov, B.: Practical byzantine fault tolerance. In: Proceedings of the Third USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 173\u2013186 (1999)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Computer Aided Verification, CAV \u201998, vol.\u00a01427, pp. 147\u2013158 (1998)","DOI":"10.1007\/BFb0028741"},{"issue":"3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"1\/2","key":"21_CR15","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1\/2), 77\u2013104 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-030-32101-7_2","volume-title":"Financial Cryptography and Data Security","author":"P Daian","year":"2019","unstructured":"Daian, P., Pass, R., Shi, E.: Snow White: robustly reconfigurable consensus and applications to provably secure proof of stake. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 23\u201341. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_2"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI (2014)","DOI":"10.1007\/978-3-642-54013-4_10"},{"issue":"2","key":"21_CR18","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N.A., Stockmeyer, L.J.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Exploiting symmetry when model-checking software. In: Formal Methods for Protocol Engineering and Distributed Systems (1999)","DOI":"10.1007\/978-0-387-35578-8_15"},{"issue":"7","key":"21_CR20","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Maung Maung\u00a0Thin, W.Y., Dong, N., Bai, G., Dong, J.S.: Formal analysis of a proof-of-stake blockchain. In: 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 197\u2013200 (2018)","DOI":"10.1109\/ICECCS2018.2018.00031"},{"key":"21_CR22","unstructured":"Milosevic, Z., Konnov, I.: Tendermint consensus tla+ model (2021). https:\/\/tinyurl.com\/26j6vfd7"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"key":"21_CR24","unstructured":"Team, T.C.: What is tendermint. https:\/\/tinyurl.com\/4ewab889"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Tholoniat, P., Gramoli, V.: Formal Verification of Blockchain Byzantine Fault Tolerance, pp. 389\u2013412. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-07535-3_12","DOI":"10.1007\/978-3-031-07535-3_12"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the raft consensus protocol. In: ACM SIGPLAN Conference on Certified Programs and Proofs (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Xu, J., Wang, C., Jia, X.: A survey of blockchain consensus protocols. ACM Comput. Surv. 55(13s) (2023)","DOI":"10.1145\/3579845"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Yoo, J., Jung, Y., Shin, D., Bae, M., Jee, E.: Formal modeling and verification of a federated byzantine agreement algorithm for blockchain platforms. In: IEEE International Workshop on Blockchain Oriented Software Engineering (2019)","DOI":"10.1109\/IWBOSE.2019.8666514"}],"container-title":["Lecture Notes in Computer Science","Engineering of Complex Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00828-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T04:05:36Z","timestamp":1779768336000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00828-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,17]]},"ISBN":["9783032008275","9783032008282"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00828-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,17]]},"assertion":[{"value":"17 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All versions of our models and detailed proofs are available at\n                      \n                      . The PAT model checker can be downloaded at\n                      \n                      .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"ICECCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Engineering of Complex Computer Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"2 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iceccs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/iceccs2025-hangzhou.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}