Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability

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).