{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T20:53:32Z","timestamp":1777064012374,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2026,4,26]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"313","volume-title":"Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018","author":"Zamansky Anna","year":"2018","unstructured":"Anna Zamansky, Maria Spichkova, Guillermo Rodr\u00edguez-Navas, Peter Herrmann, and Jan Olaf Blech. Towards Classification of Light-weight Formal Methods. In Ernesto Damiani, George Spanoudakis, and Leszek A. Maciaszek, editors, Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018, Funchal, Madeira, Portugal, March 23\u201324, 2018, pages 305\u2013313. SciTePress, 2018. ISBN 978-989-758-300-1. 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."},{"issue":"6","key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","first-page":"1756","DOI":"10.14778\/3725688.3725704","article-title":"On Optimizing Distributed Transactions in a Multi-region Data Store with True-time Clocks","volume":"18","author":"Song Haoze","year":"2025","unstructured":"Haoze Song, Yongqi Wang, Xusheng Chen, Hao Feng, Yazhi Feng, Xieyun Fang, Heming Cui, and Linghe Kong. K2: On Optimizing Distributed Transactions in a Multi-region Data Store with True-time Clocks. Proc. VLDB Endow., 18(6):1756\u20131769, 2025. URL https:\/\/www.vldb.org\/pvldb\/vol18\/p1756-song.pdf.","journal-title":"Proc. VLDB Endow."},{"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."},{"issue":"6","key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/2499370.2462184","volume":"48","author":"Desai Ankush","year":"2013","unstructured":"Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. P: Safe Asynchronous Event-Driven Programming. ACM SIGPLAN Notices, 48(6):321\u2013332, 2013.","journal-title":"Safe Asynchronous Event-Driven Programming. ACM SIGPLAN Notices"},{"issue":"1","key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/1735970.1736040","article-title":"A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs","volume":"38","author":"Burckhardt Sebastian","year":"2010","unstructured":"Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs. ACM SIGARCH Computer Architecture News, 38(1):167\u2013178, 2010.","journal-title":"ACM SIGARCH Computer Architecture News"},{"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","first-page":"12","volume-title":"2023 IEEE\/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)","author":"Hackett Finn","year":"2023","unstructured":"Finn Hackett, Joshua Rowe, and Markus Alexander Kuppe. Understanding Inconsistency in Azure Cosmos DB with TLA+. In 2023 IEEE\/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pages 1\u201312, 2023. 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","first-page":"379","volume-title":"International Conference on Computer Aided Verification","author":"Wolf Felix A","unstructured":"Felix A Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo\u00e3o C Pereira, and Peter M\u00fcller. Gobra: Modular specification and verification of go programs. In International Conference on Computer Aided Verification, pages 367\u2013379. Springer, 2021."},{"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."},{"issue":"10","key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Richard Hoare Charles Antony","year":"1969","unstructured":"Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576\u2013580, 1969.","journal-title":"Communications of the ACM"},{"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","volume-title":"Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, NSDI '25, USA","author":"Howard Heidi","year":"2025","unstructured":"Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou, and Natacha Crooks. Smart casual verification of the confidential consortium framework. In Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, NSDI '25, USA, 2025. USENIX Association. ISBN 978-1-939133-46-5."},{"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","first-page":"143","volume-title":"Tao Huang. Model Checking Guided Testing for Distributed Systems. In Proceedings of the Eighteenth European Conference on Computer Systems, EuroSys '23","author":"Wang Dong","year":"2023","unstructured":"Dong Wang, Wensheng Dou, Yu Gao, Chenao Wu, Jun Wei, and Tao Huang. Model Checking Guided Testing for Distributed Systems. In Proceedings of the Eighteenth European Conference on Computer Systems, EuroSys '23, page 127\u2013143, New York, NY, USA, 2023. Association for Computing Machinery. ISBN 9781450394871. 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","first-page":"258","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19","author":"Chajed Tej","year":"2019","unstructured":"Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, page 243\u2013258, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781450368735. 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","first-page":"370","volume-title":"International conference on logic for programming artificial intelligence and reasoning","author":"Leino K Rustan M","unstructured":"K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pages 348\u2013370. Springer, 2010."},{"key":"e_1_3_2_1_34_1","first-page":"2521","volume-title":"Yongwei Yuan. Formally Verified Cloud-Scale Authorization. In 2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE)","author":"Chakarov Aleks","year":"2025","unstructured":"Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, and Yongwei Yuan. Formally Verified Cloud-Scale Authorization. In 2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE), pages 2508\u20132521, 2025. 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":[],"deposited":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T20:26:44Z","timestamp":1777062404000},"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"}}]}}