{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:11:46Z","timestamp":1781007106404,"version":"3.54.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["2019285,1763399,2313433,2118851"],"award-info":[{"award-number":["2019285,1763399,2313433,2118851"]}]},{"name":"DARPA","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Achieving consensus is a challenging and ubiquitous problem in distributed systems that is only made harder by the introduction of malicious byzantine servers. While significant effort has been devoted to the benign and byzantine failure models individually, no prior work has considered the mechanized verification of both in a generic way. We claim this is due to the lack of an appropriate abstraction that is capable of representing both benign and byzantine consensus without either losing too much detail or becoming impractically complex. We build on recent work on the atomic distributed object model to fill this void with a novel abstraction called AdoB. In addition to revealing important insights into the essence of consensus, this abstraction has practical benefits for easing distributed system verification. As a case study, we proved safety and liveness properties for AdoB in Coq, which are the first such mechanized proofs to handle benign and byzantine consensus in a unified manner. We also demonstrate that AdoB faithfully models real consensus protocols by proving it is refined by standard network-level specifications of Fast Paxos and a variant of Jolteon.<\/jats:p>","DOI":"10.1145\/3649826","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"419-448","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8524-1978","authenticated-orcid":false,"given":"Wolf","family":"Honor\u00e9","sequence":"first","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7811-4231","authenticated-orcid":false,"given":"Longfei","family":"Qiu","sequence":"additional","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-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,4,29]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Ittai Abraham Heidi Howard and Kartik Nayak. 2021. Benign HotStuff. https:\/\/decentralizedthoughts.github.io\/2021-04-02-benign-hotstuff\/"},{"key":"e_1_2_1_2_1","unstructured":"Agda Development Team. 2005\u20132022. What is Agda? https:\/\/agda.readthedocs.io\/en\/latest\/getting-started\/what-is-agda.html"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2022.10"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.43"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2020.23"},{"key":"e_1_2_1_7_1","volume-title":"Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Ph. D. Dissertation","author":"Buchman Ethan","year":"2016","unstructured":"Ethan Buchman. 2016. Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Ph. D. Dissertation. University of Guelph."},{"key":"e_1_2_1_8_1","unstructured":"Ethan Buchman Jae Kwon and Zarko Milosevic. 2019. The Latest Gossip on BFT Consensus. arxiv:1807.04938."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1298455.1298487"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"e_1_2_1_11_1","volume-title":"Proc. of the 3rd Symposium on Operating Systems Design and Implementation (OSDI \u201999)","author":"Castro Miguel","year":"1999","unstructured":"Miguel Castro and Barbara Liskov. 1999. Practical Byzantine Fault Tolerance. In Proc. of the 3rd Symposium on Operating Systems Design and Implementation (OSDI \u201999). USENIX Association, Berkeley, CA, USA. 173\u2013186. http:\/\/dl.acm.org\/citation.cfm?id=296806.296824"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365815.1365816"},{"key":"e_1_2_1_13_1","volume-title":"Workshop on Knowledge Exchange: Automated Provers and Proof Assistants, Renate Schmidt Stephan Schulz, Piotr Rudnicki, Geoff Sutcliffe, Boris Konev (Ed.) (KEAPPA \u201908","volume":"37","author":"Chaudhuri Kaustuv C","year":"2008","unstructured":"Kaustuv C Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. 2008. A TLA+ Proof System. In Workshop on Knowledge Exchange: Automated Provers and Proof Assistants, Renate Schmidt Stephan Schulz, Piotr Rudnicki, Geoff Sutcliffe, Boris Konev (Ed.) (KEAPPA \u201908, Vol. 418). CEUR-WS.org, online. 17\u201337. http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-418\/paper2.pdf"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_13"},{"key":"e_1_2_1_15_1","unstructured":"Coq Development Team. 1999\u20132022. The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"key":"e_1_2_1_16_1","unstructured":"Jeff Dean. 2009. Designs Lessons and Advice from Building Large Distributed Systems. https:\/\/research.cs.cornell.edu\/ladis2009\/talks\/dean-keynote-ladis2009.pdf Keynote from ACM SIGOPS International Workshop on Large Scale Distributed Systems and Middleware"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"e_1_2_1_18_1","unstructured":"etcd Authors. 2013\u20132022. etcd. https:\/\/etcd.io\/"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_1_20_1","volume-title":"Proc. of the 26th International Conference on Financial Cryptography and Data Security (FC \u201922)","author":"Gelashvili Rati","year":"2022","unstructured":"Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. 2022. Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback. In Proc. of the 26th International Conference on Financial Cryptography and Data Security (FC \u201922). Springer-Verlag, Berlin, Heidelberg. https:\/\/fc22.ifca.ai\/preproceedings\/35.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945450"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132757"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Wolf Honor\u00e9 Longfei Qiu Yoonseung Kim Ji-Yong Shin Jieung Kim and Zhong Shao. 2024. AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/adob.html","DOI":"10.1145\/3649826"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Wolf Honor\u00e9 Longfei Qiu Yoonseung Kim Ji-Yong Shin Jieung Kim and Zhong Shao. 2024. Artifact For \"AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects\". https:\/\/doi.org\/10.5281\/zenodo.10727570 10.5281\/zenodo.10727570","DOI":"10.5281\/zenodo.10727570"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855840.1855851"},{"key":"e_1_2_1_29_1","unstructured":"Isabelle Development Team. 1986\u20132022. What is Isabelle? https:\/\/isabelle.in.tum.de\/overview.html"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075029.2075058"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Leslie Lamport Robert Shostak and Marshall Pease. 1982. The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems July 382\u2013401. https:\/\/doi.org\/10.1145\/357172.357176 10.1145\/357172.357176","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_36_1","volume-title":"10th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201912)","author":"Li Cheng","year":"2012","unstructured":"Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Pregui\u00e7a, and Rodrigo Rodrigues. 2012. Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201912). USENIX Association, Hollywood, CA. 265\u2013278. https:\/\/www.usenix.org\/conference\/osdi12\/technical-sessions\/presentation\/li"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.FMBC.2020.9"},{"key":"e_1_2_1_38_1","unstructured":"David Mazieres. 2015. The Stellar Consensus Protocol: A Federated Model for Internet-Level Consensus. https:\/\/www.stellar.org\/papers\/stellar-consensus-protocol"},{"key":"e_1_2_1_39_1","volume-title":"Bitcoin: A Peer-to-Peer Electronic Cash System. Decentralized Business Review.","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Decentralized Business Review."},{"key":"e_1_2_1_40_1","volume-title":"USENIX Annual Technical Conference. USENIX Association","author":"Ongaro Diego","unstructured":"Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In USENIX Annual Technical Conference. USENIX Association, Berkeley, CA, USA. 305\u2013319. https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2010.5544299"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1093\/rfs\/hhaa075"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45539-6_15"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_1_51_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\/3649826","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":51,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649826"],"URL":"https:\/\/doi.org\/10.1145\/3649826","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}