{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:56Z","timestamp":1784196596392,"version":"3.55.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2019285, 2313433"],"award-info":[{"award-number":["2019285, 2313433"]}],"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":[[2025,6,10]]},"abstract":"<jats:p>Blockchains operating at the global scale demand high-performance byzantine fault-tolerant (BFT) consensus protocols. Most classic PBFT-like protocols suffer from an issue known as the leader bottleneck, which severely limits their throughput and resource utilization. Recently, Directed Acyclic Graph, or DAG-based protocols, have emerged as a promising approach for eliminating the leader bottleneck and achieving better performance. They attain higher throughput by separating data dissemination and block ordering. However, their safety and liveness logic is also significantly more elaborate. So far, most DAG-based protocols have only enjoyed on-paper security proofs, and it is not clear how to construct formal proofs of these protocols efficiently.<\/jats:p>\n                  <jats:p>We introduce LiDO-DAG, a concurrent object model that abstracts the common logic of these protocols. LiDO-DAG is constructed by combining a DAG abstraction and LiDO, a recently proposed abstraction for leader-based consensus. To demonstrate that our framework enables rapid validation of new DAG-based protocol designs, we implemented LiDO-DAG in Coq and applied it to three recent DAG-based protocols, including Narwhal, Bullshark, and Sailfish. Our framework readily yields mechanized safety and liveness proofs for all three protocols, which are also the first mechanized liveness proofs of any DAG-based protocol. Our framework has also revealed an optimization for Sailfish that improves its worst-case latency.<\/jats:p>","DOI":"10.1145\/3729306","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1392-1416","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols"],"prefix":"10.1145","volume":"9","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\/0009-0003-9430-6165","authenticated-orcid":false,"given":"Jingqi","family":"Xiao","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-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":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Balaji Arun Zekun Li Florian Suri-Payer Sourav Das and Alexander Spiegelman. 2024. Shoal++: High Throughput DAG BFT Can Be Fast! arXiv:2405.20488 [cs.DC] https:\/\/arxiv.org\/abs\/2405.20488"},{"key":"e_1_3_2_3_1","doi-asserted-by":"crossref","unstructured":"Kushal Babel Andrey Chursin George Danezis Anastasios Kichidis Lefteris Kokoris-Kogias Arun Koshy Alberto Sonnino and Mingwei Tian. 2024. Mysticeti: Reaching the Limits of Latency with Uncertified DAGs. arXiv:2310.14821 [cs.DC] https:\/\/arxiv.org\/abs\/2310.14821","DOI":"10.14722\/ndss.2025.240929"},{"key":"e_1_3_2_4_1","volume-title":"The swirlds hashgraph consensus algorithm: Fair, fast, byzantine fault tolerance","author":"Baird Leemon","year":"2016","unstructured":"Leemon Baird. 2016. The swirlds hashgraph consensus algorithm: Fair, fast, byzantine fault tolerance. Technical Report SWIRLDS-TR-2016-01. Swirlds. https:\/\/www.swirlds.com\/downloads\/SWIRLDS-TR-2016-01.pdf"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_3_2_6_1","unstructured":"Nathalie Bertrand Pranav Ghorpade Sasha Rubin Bernhard Scholz and Pavle Subotic. 2024. Reusable Formal Verification of DAG-based Consensus Protocols. arXiv:2407.02167 [cs.LO] https:\/\/arxiv.org\/abs\/2407.02167"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.10"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00603-x"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.12"},{"key":"e_1_3_2_10_1","unstructured":"Ethan Buchman Jae Kwon and Zarko Milosevic. 2019. The latest gossip on BFT consensus. arXiv:2212.08073 [cs.DC] https:\/\/arxiv.org\/abs\/1807.04938"},{"key":"e_1_3_2_11_1","unstructured":"Vitalik Buterin. 2014. Ethereum: A Next-Generation Smart Contract and Decentralized Application Platform. https:\/\/ethereum.org\/content\/whitepaper\/whitepaper-pdf\/Ethereum_Whitepaper_-_Buterin_2014.pdf"},{"key":"e_1_3_2_12_1","unstructured":"Vitalik Buterin. 2024. Possible futures of the Ethereum protocol part 2: The Surge. https:\/\/vitalik.eth.limo\/general\/2024\/10\/17\/futures2.html"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"e_1_3_2_14_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_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_13"},{"key":"e_1_3_2_16_1","unstructured":"CoinGecko. 2024. Top Blockchains by Total Value Locked (TVL). https:\/\/www.coingecko.com\/en\/chains"},{"key":"e_1_3_2_17_1","unstructured":"Karl Crary. 2021. Verifying the Hashgraph Consensus Algorithm. arXiv:2212.08073 [cs.LO] https:\/\/arxiv.org\/abs\/2102.01167"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492321.3519594"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-18283-9_14"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318041.3355467"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3465084.3467905"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.DISC.2023.26"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(1:5)2023"},{"key":"e_1_3_2_30_1","doi-asserted-by":"crossref","unstructured":"Andrew Lewis-Pye Dahlia Malkhi Oded Naor and Kartik Nayak. 2024. Lumiere: Making Optimal BFT for Partial Synchrony Practical. arXiv:2212.08073 [cs.DC] https:\/\/arxiv.org\/abs\/2311.08091","DOI":"10.1145\/3662158.3662787"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.FMBC.2020.9"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.Tokenomics.2022.6"},{"key":"e_1_3_2_33_1","unstructured":"Satoshi Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.21428\/58320208.08912a03"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483584"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10909272"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656423"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Longfei Qiu Jingqi Xiao Ji Yong Shin and Zhong Shao. 2025a. Artifact for PLDI 2025 Paper #316 LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols. https:\/\/doi.org\/10.5281\/zenodo.15223659 10.5281\/zenodo.15223659","DOI":"10.5281\/zenodo.15223659"},{"key":"e_1_3_2_40_1","volume-title":"LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols","author":"Qiu Longfei","year":"2025","unstructured":"Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao. 2025b. LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols. Technical Report TR1574. Yale Univ. https:\/\/flint.cs.yale.edu\/publications\/lido-dag.html"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/icbc59979.2024.10634358"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP61157.2025.00021"},{"key":"e_1_3_2_44_1","unstructured":"Alexander Spiegelman Balaji Arun Rati Gelashvili and Zekun Li. 2023. Shoal: Improving DAG-BFT Latency And Robustness. arXiv:2306.03058 [cs.DC] https:\/\/arxiv.org\/abs\/2306.03058"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3559361"},{"key":"e_1_3_2_46_1","doi-asserted-by":"crossref","unstructured":"Alexander Spiegelman Neil Giridharan Alberto Sonnino and Lefteris Kokoris-Kogias. 2022b. Bullshark: The Partially Synchronous Version. arXiv:2209.05633 [cs.DC] https:\/\/arxiv.org\/abs\/2209.05633","DOI":"10.1145\/3548606.3559361"},{"key":"e_1_3_2_47_1","volume-title":"Proceedings of the 18th USENIX Conference on Operating Systems Design and Implementation (Santa Clara, CA, USA) (OSDI\u201924).","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: verifying liveness of cluster management controllers. In Proceedings of the 18th USENIX Conference on Operating Systems Design and Implementation (Santa Clara, CA, USA) (OSDI\u201924). USENIX Association, USA, Article 35, 18 pages."},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192414"},{"key":"e_1_3_2_49_1","unstructured":"The Coq Development Team. 2024. The Coq Reference Manual \u2013 Release 8.19.0. https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman."},{"key":"e_1_3_2_50_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_2_51_1","unstructured":"Visa Inc. 2023. Annual Report 2023. https:\/\/s29.q4cdn.com\/385744025\/files\/doc_downloads\/2023\/Visa-Inc-Fiscal-2023-Annual-Report.pdf"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360564"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331591"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690355"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729306","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729306","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:01:46Z","timestamp":1784196106000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729306"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":55,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729306"],"URL":"https:\/\/doi.org\/10.1145\/3729306","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}