49 - Formal Verification of a Distributed Algorithm

Distributed systems algorithms are notoriously difficult to reason about correctly: subtle bugs can arise from unexpected message exchanges, concurrent memory access, improper resource usage, or other violations of intended invariants, and such bugs often evade conventional testing. Formal verification techniques, ranging from type-system extensions and automated theorem provers to model checkers and interactive proof assistants, offer varying tradeoffs between automation and expressiveness for catching such bugs before deployment. This project applies a formal verification approach (specific technique and tooling TBD) to a distributed algorithm, with the goal of specifying and verifying a key correctness property. We report on the process of formalizing the algorithm and its invariants, the extent to which verification could be automated versus required manual guidance, and any bugs or limitations of the algorithm or the verification approach uncovered along the way. This work aims to assess the practicality of the chosen verification technique for distributed systems code and to identify any extensions needed to express distributed-systems-specific properties.