{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:20Z","timestamp":1787592260883,"version":"build-2736575974"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    Strongly-consistent replicated data stores are a popular foundation for many kinds of online services, but their implementations are very complex. Strong replication is not\n                    <jats:italic toggle=\"yes\">available<\/jats:italic>\n                    under network partitions, and so achieving a functional degree of fault-tolerance requires correctly implementing\n                    <jats:italic toggle=\"yes\">consensus algorithms<\/jats:italic>\n                    like Raft and Paxos. These algorithms are notoriously difficult to reason about, and many data stores implement custom variations to support unique performance tradeoffs, presenting an opportunity for automated verification tools. Unfortunately, existing tools that have been applied to distributed consensus demand too much developer effort, a problem stemming from the low-level programming model in which consensus and strong replication are implemented\u2014asynchronous message passing\u2014which thwarts decidable automation by exposing the details of asynchronous communication.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we consider the implementation and automated verification of strong replication systems\n                    <jats:italic toggle=\"yes\">as applications<\/jats:italic>\n                    of weak replicated data stores. Weak stores, being available under partition, are a suitable foundation for performant distributed applications. Crucially, they abstract asynchronous communication and allow us to derive local-scope conditions for the verification of consensus safety. To evaluate this approach, we have developed a verified-programming framework for the weak replicated state model, called Super-V. This framework enables SMT-based verification based on local-scope artifacts called\n                    <jats:italic toggle=\"yes\">stable update preconditions,<\/jats:italic>\n                    replacing standard-practice global inductive invariants. We have used our approach to implement and verify a strong replication system based on an adaptation of the Raft consensus algorithm.\n                  <\/jats:p>","DOI":"10.1145\/3720502","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1604-1631","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Bolt-On Strong Consistency: Specification, Implementation, and Verification"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0469-1991","authenticated-orcid":false,"given":"Nicholas V.","family":"Lewchenko","sequence":"first","affiliation":[{"name":"University of Colorado Boulder, Boulder, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4189-3189","authenticated-orcid":false,"given":"Gowtham","family":"Kaki","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, Boulder, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1954-0774","authenticated-orcid":false,"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, Boulder, USA"},{"name":"Amazon, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3299869.3319893"},{"key":"e_1_3_1_3_1","unstructured":"Peter Alvaro Neil Conway Joseph M. Hellerstein and William R. Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach. In Fifth Biennial Conference on Innovative Data Systems Research CIDR 2011 Asilomar CA USA January 9-12 2011 Online Proceedings. www.cidrdb.org 249\u2013260. http:\/\/cidrdb.org\/cidr2011\/Papers\/CIDR11_Paper35.pdf"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450142.2450151"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2596631.2596633"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/226643.226647"},{"key":"e_1_3_1_10_1","unstructured":"Confluent. 2024. Kafka Raft Metadata Mode. https:\/\/docs.confluent.io\/platform\/current\/kafka-metadata\/kraft.html."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491245"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.9"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_3_1_14_1","unstructured":"etcd. 2024. etcd: a distributed reliable key-value store. https:\/\/github.com\/etcd-io\/etcd. Accessed: 2024-10-15."},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/277697.277724"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_3_1_20_1","unstructured":"Tobias Grieger. 2019. Joint Consensus in Raft. https:\/\/www.cockroachlabs.com\/blog\/joint-consensus-raft\/. Accessed: March 4 2025."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2016.25"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_14"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_1_27_1","volume-title":"Generalized Consensus and Paxos","author":"Lamport Leslie","year":"2004","unstructured":"Leslie Lamport. 2004. Generalized Consensus and Paxos. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/tr-2005-33.pdf"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Nicholas V. Lewchenko Gowtham Kaki and Bor-Yuh Evan Chang. 2025. Artifact for Bolt-On Strong Consistency: Specification Implementation and Verification. doi:10.5281\/zenodo.14948229","DOI":"10.5281\/zenodo.14948229"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_3_1_31_1","volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","year":"1996","unstructured":"Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_3_1_32_1","unstructured":"Dmitry Martyanov. 2020. CRDT in Production. https:\/\/www.infoq.com\/presentations\/crdt-production\/. Accessed: March 4 2025."},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_26"},{"key":"e_1_3_1_35_1","first-page":"305","volume-title":"Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (Philadelphia, PA) (USENIX ATC\u201914)","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (Philadelphia, PA) (USENIX ATC\u201914). USENIX Association, USA, 305\u2013320."},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3587216.3587222"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2021.61"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_1_45_1","unstructured":"Pedro Teixeira. 2017. Decentralized Real-Time Collaborative Documents - Conflict-free editing in the browser using js-ipfs and CRDTs. https:\/\/ipfs.io\/blog\/30-js-ipfs-crdts.md."},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_3_1_47_1","unstructured":"Evan Wallace. 2019. How Figma\u2019s Multiplayer Technology Works. https:\/\/www.figma.com\/blog\/how-figmas-multiplayer-technology-works\/. Accessed: March 4 2025."},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591276"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720502","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:53Z","timestamp":1787589113000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720502"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":49,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720502"],"URL":"https:\/\/doi.org\/10.1145\/3720502","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}