Shipwright: Proving liveness of distributed systems with Byzantine participants

Derek Leung, Nickolai Zeldovich, Frans Kaashoek

Ensuring liveness in a decentralized system, such as PBFT, is critical, because there may not be any single administrator that can restart the system if it encounters a liveness bu…