LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs

Explore a groundbreaking 17-minute video presentation from PLDI 2024 introducing LiDO, a consensus model for verifying both safety and liveness in Byzantine fault-tolerant state machine replication protocols. Delve into the challenges of implementing protocols like PBFT, HotStuff, and Jolteon, crucial for modern blockchain technologies. Discover how LiDO addresses the gap in liveness verification for popular partially synchronous protocols by incorporating a pacemaker state. Learn about the mechanized safety and liveness proofs for unpipelined and pipelined Jolteon in Coq, marking the first such proof for a Byzantine consensus protocol with advanced optimizations. Gain insights into distributed systems, consensus protocols, and formal verification techniques presented by researchers from Yale University, Northeastern University, and Inha University.