Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability

Proceedings of the 21st European Conference on Computer Systems 2026 Open access

Read full text
Authors: Claudia Cauli, Timo Lang, Shuo Chen, Sebti Mouelhi, Xin Jin, Subhajit Bandopadhyay, Xusheng Chen, Yazhi Feng, Haoze Song, Linhua Tang, Zhenli Sheng, Ananth Shrinivas Srinath
DOI: 10.1145/3767295.3803626
Cited by: 1
References: 8

Abstract

Formal methods are increasingly adopted in systems where reliability and correctness are critical, enabled by improvements in tool usability, speed, and automation. This industrial experience report presents three projects at Huawei Cloud showcasing different trade-offs in investment and assurance levels. We applied probabilistic concurrency testing, model checking, and deductive verification to two foundational services in the database and networking domains: the K2 transactional key-value store and the Global Server Load Balancer (GSLB).

Fields of Study & Subjects

Power System Reliability and Maintenance Reliability and Maintenance Optimization Software Reliability and Analysis Research

Publication details

Journal / source
Proceedings of the 21st European Conference on Computer Systems
Publisher
ACM
Pages
2223–2238
Publication date
24 April 2026