{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:10:24Z","timestamp":1783008624522,"version":"3.54.5"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2019285, 1763399, 2313433, 2118851"],"award-info":[{"award-number":["2019285, 1763399, 2313433, 2118851"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Byzantine fault-tolerant state machine replication (SMR) protocols, such as PBFT, HotStuff, and Jolteon, are essential for modern blockchain technologies. However, they are challenging to implement correctly because they have to deal with any unexpected message from Byzantine peers and ensure safety and liveness at all times. Many formal frameworks have been developed to verify the safety of SMR implementations, but there is still a gap in the verification of their liveness. Existing liveness proofs are either limited to the network level or do not cover popular partially synchronous protocols.<\/jats:p>\n          <jats:p>We introduce LiDO, a consensus model that enables the verification of both safety and liveness of implementations through refinement. We observe that current consensus models cannot handle liveness because they do not include a pacemaker state. We show that by adding a pacemaker state to the LiDO model, we can express the liveness properties of SMR protocols as a few safety properties that can be easily verified by refinement proofs. Based on our LiDO model, we provide mechanized safety and liveness proofs for both unpipelined and pipelined Jolteon in Coq. This is the first mechanized liveness proof for a byzantine consensus protocol with non-trivial optimizations such as pipelining.<\/jats:p>","DOI":"10.1145\/3656423","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1140-1164","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-7811-4231","authenticated-orcid":false,"given":"Longfei","family":"Qiu","sequence":"first","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5294-1046","authenticated-orcid":false,"given":"Yoonseung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1595-4849","authenticated-orcid":false,"given":"Ji-Yong","family":"Shin","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7581-041X","authenticated-orcid":false,"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Inha University, Incheon, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8524-1978","authenticated-orcid":false,"given":"Wolf","family":"Honor\u00e9","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3465084.3467953"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Idan Berkovits Marijana Lazi\u0107 Giuliano Losa Oded Padon and Sharon Shoham. 2019. Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In Computer Aided Verification Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing Cham 245\u2013266. https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15 10.1007\/978-3-030-25543-5_15","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.10"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.43"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.12"},{"key":"e_1_3_1_7_1","unstructured":"Vitalik Buterin Diego Hernandez Thor Kamphefner Khiem Pham Zhi Qiao Danny Ryan Juhyeok Sin Ying Wang and Yan X Zhang. 2020. Combining GHOST and Casper. arXiv:2003.03052 [cs.CR]"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"e_1_3_1_9_1","volume-title":"Practical Byzantine Fault Tolerance","author":"Castro Miguel","year":"2001","unstructured":"Miguel Castro. 2001. Practical Byzantine Fault Tolerance. Ph. D. Dissertation. Massachusetts Institute of Technology. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/01\/thesis-mcastro.pdf"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_13"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.14"},{"key":"e_1_3_1_12_1","unstructured":"Francesco D\u2019Amato Joachim Neu Ertem Nusret Tas and David Tse. 2023. Goldfish: No More Attacks on Ethereum?! arXiv:2209.03255 [cs.CR]"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-18283-9_14"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583668.3594572"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649826"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-56877-1_16"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419614.3423263"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_1_27_1","unstructured":"Leslie Lamport. 2005. Real Time is Really Simple. Technical Report MSR-TR-2005-30. 72 pages. https:\/\/www.microsoft.com\/en-us\/research\/publication\/real-time-is-really-simple\/"},{"key":"e_1_3_1_28_1","unstructured":"Andrew Lewis-Pye. 2022. Quadratic worst-case message complexity for State Machine Replication in the partial synchrony model. CoRR abs\/2201.01107 (2022). arXiv:2201.01107"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.FMBC.2020.9"},{"key":"e_1_3_1_30_1","article-title":"Extended Abstract: HotStuff-2: Optimal Two-Phase Responsive BFT","volume":"2023","author":"Malkhi Dahlia","year":"2023","unstructured":"Dahlia Malkhi and Kartik Nayak. 2023. Extended Abstract: HotStuff-2: Optimal Two-Phase Responsive BFT. Cryptology ePrint Archive, Paper 2023\/397. https:\/\/eprint.iacr.org\/2023\/397","journal-title":"Cryptology ePrint Archive, Paper"},{"issue":"2","key":"e_1_3_1_31_1","article-title":"Cogsworth: Byzantine View Synchronization","volume":"1","author":"Naor Oded","year":"2021","unstructured":"Oded Naor, Mathieu Baudet, Dahlia Malkhi, and Alexander Spiegelman. 2021. Cogsworth: Byzantine View Synchronization. Cryptoeconomic Systems 1, 2 (oct 22 2021). https:\/\/doi.org\/10.21428\/58320208.08912a03","journal-title":"Cryptoeconomic Systems"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Oded Naor and Idit Keidar. 2020. Expected Linear Round Synchronization: The Missing Link for Linear Byzantine SMR. In 34th International Symposium on Distributed Computing (DISC 2020) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 179) Hagit Attiya (Ed.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 26:1\u201326:17. https:\/\/doi.org\/10.4230\/LIPIcs.DISC.2020.26 10.4230\/LIPIcs.DISC.2020.26","DOI":"10.4230\/LIPIcs.DISC.2020.26"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10909272"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656423"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192414"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"S\u00f8ren Eller Thomsen and Bas Spitters. 2021. Formalizing Nakamoto-Style Proof of Stake. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF). 1\u201315. https:\/\/doi.org\/10.1109\/CSF51468.2021.00042 10.1109\/CSF51468.2021.00042","DOI":"10.1109\/CSF51468.2021.00042"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331591"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656423","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656423","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:38Z","timestamp":1751661818000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656423"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":44,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656423"],"URL":"https:\/\/doi.org\/10.1145\/3656423","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}