{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T07:02:23Z","timestamp":1782975743573,"version":"3.54.5"},"reference-count":46,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"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":["HR00112590130"],"award-info":[{"award-number":["HR00112590130"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,18]]},"DOI":"10.1109\/sp63933.2026.00009","type":"proceedings-article","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T19:34:20Z","timestamp":1782934460000},"page":"1842-1861","source":"Crossref","is-referenced-by-count":0,"title":["Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol Under the LiDO-DAG Framework"],"prefix":"10.1109","author":[{"given":"Longfei","family":"Qiu","sequence":"first","affiliation":[{"name":"Yale University,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jingqi","family":"Xiao","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","volume-title":"Bitcoin: A peer-to-peer electronic cash system","author":"Nakamoto","year":"2008"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.cosust.2017.04.011","article-title":"Sustainability of bitcoin and blockchains","volume":"28","author":"Vranken","year":"2017","journal-title":"Current Opinion in Environmental Sustainability"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2023.3302955"},{"key":"ref4","volume-title":"Combining ghost and casper","author":"Buterin","year":"2020"},{"key":"ref5","volume-title":"The aptos blockchain: Safe, scalable, and upgradeable web3 infrastructure","year":"2022"},{"key":"ref6","volume-title":"Practical byzantine fault tolerance","author":"Castro","year":"2001"},{"key":"ref7","volume-title":"The latest gossip on bft consensus","author":"Buchman","year":"2019"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331591"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-18283-9_14"},{"issue":"2","key":"ref10","article-title":"Cogsworth: Byzantine View Synchronization","volume":"1","author":"Naor","year":"2021","journal-title":"Cryptoeconomic Systems"},{"key":"ref11","volume-title":"Lumiere: Making optimal bft for partial synchrony practical","author":"Lewis-Pye","year":"2024"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3492321.3519594"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483584"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3465084.3467905"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3559361"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/sp61157.2025.00021"},{"key":"ref17","article-title":"Cordial miners: Fast and efficient consensus for every eventuality","author":"Keidar","year":"2023","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"ref18","volume-title":"Mysticeti: Reaching the limits of latency with uncertified dags","author":"Babel","year":"2024"},{"key":"ref19","volume-title":"Shoal: Improving dag-bft latency and robustness","author":"Spiegelman","year":"2023"},{"issue":"2","key":"ref20","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/0890-5401(87)90054-X","article-title":"Asynchronous byzantine agreement protocols","volume":"75","author":"Bracha","year":"1987","journal-title":"Information and Computation"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/RELDIS.2005.9"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484808"},{"key":"ref23","volume-title":"Iota rebased: Fast forward","year":"2024"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3656423"},{"key":"ref28","doi-asserted-by":"crossref","DOI":"10.1145\/3729306","article-title":"LiDO-DAG: A framework for verifying safety and liveness of dag-based consensus protocols","volume-title":"Yale Univ., Tech. Rep.","author":"Qiu","year":"2025"},{"key":"ref29","volume-title":"Artifact for s&p 2026 paper #131 mechanized safety and liveness proofs for the mysticeti consensus protocol under the lido-dag framework","author":"Qiu","year":"2025"},{"key":"ref30","article-title":"Starfish: A high throughput BFT protocol on uncertified DAG with linear amortized communication complexity","author":"Polyanskii","year":"2025","journal-title":"Cryptology ePrint Archive"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"ref33","first-page":"12:1","article-title":"Liveness and latency of byzantine state-machine replication","volume-title":"36th International Symposium on Distributed Computing, DISC 2022","volume":"246","author":"Bravo","year":"2022"},{"key":"ref34","article-title":"Real time is really simple","volume-title":"Tech. Rep.","author":"Lamport","year":"2005"},{"key":"ref35","volume-title":"Sui."},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3689778"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_14"},{"key":"ref42","volume-title":"Reusable formal verification of dag-based consensus protocols","author":"Bertrand","year":"2024"},{"key":"ref43","volume-title":"Formal verification of blockchain nonforking in dag-based bft consensus with dynamic stake","author":"Coglio","year":"2025"},{"key":"ref44","volume-title":"Verifying the hashgraph consensus algorithm","author":"Crary","year":"2021"},{"key":"ref45","article-title":"The swirlds hashgraph consensus algorithm: Fair, fast, byzantine fault tolerance","volume-title":"Swirlds, Tech. Rep.","author":"Baird","year":"2016"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00042"}],"event":{"name":"2026 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2026,5,18]]},"end":{"date-parts":[[2026,5,21]]}},"container-title":["2026 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11573355\/11573356\/11573364.pdf?arnumber=11573364","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T05:35:02Z","timestamp":1782970502000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11573364\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,18]]},"references-count":46,"URL":"https:\/\/doi.org\/10.1109\/sp63933.2026.00009","relation":{},"subject":[],"published":{"date-parts":[[2026,5,18]]}}}