{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T13:02:31Z","timestamp":1780664551749,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,4,26]],"date-time":"2026-04-26T00:00:00Z","timestamp":1777161600000},"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":[],"published-print":{"date-parts":[[2026,4,27]]},"DOI":"10.1145\/3767295.3803626","type":"proceedings-article","created":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T20:20:04Z","timestamp":1777062004000},"page":"2223-2238","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0029-7938","authenticated-orcid":false,"given":"Claudia","family":"Cauli","sequence":"first","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8257-968X","authenticated-orcid":false,"given":"Timo","family":"Lang","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7128-8359","authenticated-orcid":false,"given":"Shuo","family":"Chen","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5808-5631","authenticated-orcid":false,"given":"Sebti","family":"Mouelhi","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3005-4330","authenticated-orcid":false,"given":"Xin","family":"Jin","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2107-1732","authenticated-orcid":false,"given":"Subhajit","family":"Bandopadhyay","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7344-7505","authenticated-orcid":false,"given":"Xusheng","family":"Chen","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4606-8126","authenticated-orcid":false,"given":"Yazhi","family":"Feng","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5952-5168","authenticated-orcid":false,"given":"Haoze","family":"Song","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8958-756X","authenticated-orcid":false,"given":"Linhua","family":"Tang","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9127-1496","authenticated-orcid":false,"given":"Zhenli","family":"Sheng","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8502-7740","authenticated-orcid":false,"given":"Ananth Shrinivas","family":"Srinath","sequence":"additional","affiliation":[{"name":"Huawei Technologies Co., Ltd, Ireland, Dublin, Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,4,26]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5220\/0006770803050313"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689374"},{"key":"e_1_3_2_1_3_1","volume-title":"How Amazon Web Services uses formal methods. Communications of the ACM","author":"Newcombe Chris","year":"2015","unstructured":"Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon Web Services uses formal methods. Communications of the ACM, 2015. URL https:\/\/www.amazon.science\/publications\/how-amazon-web-services-uses-formal-methods."},{"key":"e_1_3_2_1_4_1","first-page":"454","volume-title":"Bryan Parno. Verus: A Practical Foundation for Systems Verification. In 2024 Symposium on Operating Systems Principles","author":"Lattuada Andrea","year":"2024","unstructured":"Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, and Bryan Parno. Verus: A Practical Foundation for Systems Verification. In 2024 Symposium on Operating Systems Principles, pages 438\u2013454, November 2024. URL https:\/\/www.microsoft.com\/en-us\/research\/publication\/verus-a-practical-foundation-for-systems-verification\/."},{"key":"e_1_3_2_1_5_1","volume-title":"HATRA 2020: Human Aspects of Types and Reasoning Assistants, 2020","author":"Reid Alastair","year":"2010","unstructured":"Alastair Reid, Shaked Flur, Luke Church, Sarah de Haas, Maritza Johnson, and Ben Laurie. Towards making formal methods normal: meeting developers where they are. In HATRA 2020: Human Aspects of Types and Reasoning Assistants, 2020. URL https:\/\/arxiv.org\/abs\/2010.16345."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.14778\/3725688.3725704"},{"key":"e_1_3_2_1_7_1","volume-title":"Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, et al. Spanner: Google's globally distributed database. ACM Transactions on Computer Systems (TOCS), 31(3):1\u201322","author":"Corbett James C","year":"2013","unstructured":"James C Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, Jeffrey John Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, et al. Spanner: Google's globally distributed database. ACM Transactions on Computer Systems (TOCS), 31(3):1\u201322, 2013."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1735970.1736040"},{"key":"e_1_3_2_1_10_1","volume-title":"Jacob Van Geffen, and Andrew Warfield. Using lightweight formal methods to validate a key-value storage node in Amazon S3","author":"Bornholt James","year":"2021","unstructured":"James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. Using lightweight formal methods to validate a key-value storage node in Amazon S3. 2021. URL https:\/\/www.amazon.science\/publications\/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3."},{"key":"e_1_3_2_1_11_1","unstructured":"Repository with P specifications. https:\/\/github.com\/deepseek-ai\/3FS\/tree\/main\/specs."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"e_1_3_2_1_14_1","volume-title":"USENIX","author":"Kuppe Markus A.","year":"2023","unstructured":"Markus A. Kuppe, Finn Hackett, and Josh Rowe. Going Beyond an Incident Report with TLA+. USENIX, July 2023. URL https:\/\/www.usenix.org\/sites\/default\/files\/login_-_going_beyond_an_incident_report_with_tla_.pdf."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.14778\/3750601.3750626"},{"key":"e_1_3_2_1_16_1","volume-title":"Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction. CoRR, abs\/2202.11385","author":"Gu Xiaosong","year":"2022","unstructured":"Xiaosong Gu, Wei Cao, Yicong Zhu, Xuan Song, Yu Huang, and Xiaoxing Ma. Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction. CoRR, abs\/2202.11385, 2022. URL https:\/\/arxiv.org\/abs\/2202.11385."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"e_1_3_2_1_18_1","first-page":"62","volume-title":"Viper: A Verification Infrastructure for Permission-Based Reasoning","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation, pages 41\u201362, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. ISBN 978-3-662-49122-5."},{"key":"e_1_3_2_1_19_1","first-page":"81","volume-title":"Program Verification: Fundamental Issues in Computer Science","author":"Floyd Robert W","unstructured":"Robert W Floyd. Assigning meanings to programs. In Program Verification: Fundamental Issues in Computer Science, pages 65\u201381. Springer, 1993."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_21_1","volume-title":"Protocols to Code: Formal Verification of a Next-Generation Internet Router. Technical report","author":"Pereira J. C.","year":"2024","unstructured":"J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. M\u00fcller, and A. Perrig. Protocols to Code: Formal Verification of a Next-Generation Internet Router. Technical report, 2024. URL https:\/\/arxiv.org\/abs\/2405.06074."},{"key":"e_1_3_2_1_22_1","unstructured":"Kyle Kingsbury. Jepsen 2025. URL https:\/\/jepsen.io\/."},{"key":"e_1_3_2_1_23_1","volume-title":"Jepsen Consistency Model","author":"Kingsbury Kyle","year":"2025","unstructured":"Kyle Kingsbury. Jepsen Consistency Model, 2025. URL https:\/\/jepsen.io\/consistency\/models."},{"key":"e_1_3_2_1_24_1","unstructured":"Atul Adya. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. MIT Cambridge MA USA March 1999. Also as Technical Report MIT\/LCS\/TR-786."},{"key":"e_1_3_2_1_25_1","unstructured":"ScyllaDB. Seastar 2025. URL https:\/\/seastar.io\/."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/3767955.3767970"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3587442"},{"key":"e_1_3_2_1_29_1","volume-title":"transition from global to modular temporal reasoning about programs, page 123\u2013144","author":"Pnueli A.","year":"1989","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs, page 123\u2013144. Springer-Verlag, Berlin, Heidelberg, 1989. ISBN 0387151818."},{"key":"e_1_3_2_1_30_1","unstructured":"gRPC Documentation. https:\/\/grpc.io\/docs\/."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_32_1","volume-title":"Electronic Notes in Theoretical Computer Science","author":"Biere Armin","year":"2002","unstructured":"Armin Biere, Cyrille Artho, and Viktor Schuppan. Liveness checking as safety checking. In Elsevier, editor, Electronic Notes in Theoretical Computer Science, 2002."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00166"},{"key":"e_1_3_2_1_35_1","unstructured":"TLA+ webpage. https:\/\/lamport.azurewebsites.net\/tla\/tla.html."},{"key":"e_1_3_2_1_36_1","unstructured":"Learn TLA+. https:\/\/learntla.com\/."},{"key":"e_1_3_2_1_37_1","unstructured":"P Language Manual. https:\/\/p-org.github.io\/P\/manualoutline\/."},{"key":"e_1_3_2_1_38_1","unstructured":"Practical Program Verification in Go with Gobra. https:\/\/viperproject.github.io\/gobra-book\/."},{"key":"e_1_3_2_1_39_1","unstructured":"A Tutorial on Gobra. https:\/\/github.com\/viperproject\/gobra\/blob\/master\/docs\/tutorial.md."},{"key":"e_1_3_2_1_40_1","unstructured":"Gobra Issue 858. https:\/\/github.com\/viperproject\/gobra\/issues\/858."}],"event":{"name":"EUROSYS '26: 21st European Conference on Computer Systems","location":"McEwan Hall\/The University of Edinburgh Edinburgh Scotland UK","acronym":"EUROSYS '26","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 21st European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3767295.3803626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T12:09:35Z","timestamp":1780661375000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3767295.3803626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,26]]},"references-count":40,"alternative-id":["10.1145\/3767295.3803626","10.1145\/3767295"],"URL":"https:\/\/doi.org\/10.1145\/3767295.3803626","relation":{},"subject":[],"published":{"date-parts":[[2026,4,26]]},"assertion":[{"value":"2026-04-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}