Inductive Invariants for Streamlining Distributed Protocol Proofs

Explore a 16-minute conference talk from USENIX OSDI '24 that introduces a novel approach to simplifying and partially automating the process of finding inductive invariants for distributed protocols. Learn about the Kondo methodology, which leverages an invariant taxonomy to divide invariants into Regular and Protocol Invariants. Discover how this approach can significantly reduce developer effort in proving the correctness of distributed protocols modeled as state machines. Gain insights into the key steps of the Kondo methodology, including manually devising Protocol Invariants, automatically generating Regular Invariants, and combining these elements into a draft proof of the asynchronous protocol. Understand the potential impact of this approach on streamlining distributed protocol proofs across a wide variety of protocols.