2025 Theses Doctoral

Automated Verification of Safety and Liveness Properties for Distributed Protocols

Yao, Jianan

The world relies on distributed systems, but these systems are increasingly complex and hard to design and implement correctly. This is due to the intrinsic non-determinism from asynchronous node communications, various failure scenarios, and potentially adversarial participants. To address this problem, developers are starting to turn to formal verification techniques to prove the correctness of distributed systems. This involves formally verifying that desired safety and liveness properties hold for the distributed protocol.

A safety property is an invariant that should hold true at any point in a system’s execution. It ensures the protocol does not reach invalid or dangerous states. A liveness property, on the contrary, describes that some desired good event will eventually happen. There have long been efforts to formally verify safety and liveness of distributed protocols. However, the proof burden is usually prohibitively high for broad real-world adoption. Although there has been a growing list of methods that try to automate the verification of distributed protocols, in particular their safety properties, none of these tools scale to real-world complex protocols with theoretical guarantee.In this dissertation, I introduce our verification methods and tools for verifying distributed protocols with little to no human effort.

The thesis consists of two parts. In the first part, I present our two inductive invariant inference tools, DistAI and DuoAI, which automatically verify safety properties of distributed protocols. In DistAI, I introduce a simulation-enumeration-refinement framework for invariant reasoning, and DuoAI extends it to more complex protocols and existential quantifiers. The evaluation shows that DuoAI outperforms alternative methods in both the number of protocols verified and the speed to verify them, including solving Paxos more than two orders of magnitude faster than any alternative method.

In the second part, I introduce LVR, our liveness verification tool for distributed protocols. The key theoretical insight is that liveness verification can be soundly reduced to the verification of a list of simpler safety properties, which can often be proved automatically utilizing an arsenal of invariant inference tools. The reduction leaves one remaining task---to synthesize a ranking function to prove termination, for which I present a new and effective pipeline. LVR is successfully applied to eight distributed protocols and is the first to demonstrate that liveness properties of distributed protocols can be proved with limited human input.