Byzantine consensus and its generalization to Byzantine state-machine replication (SMR) lie at the core of blockchains, where they ensure the consistency of replicated state even in the presence of malicious replicas. Byzantine SMR protocols often guarantee safety under all circumstances and liveness only under synchrony. However, guaranteeing liveness even under this assumption is challenging, and this has often been a source of subtle bugs. To improve this situation, I will present a modular framework to facilitate the design of provably live and efficient Byzantine SMR protocols. Our framework relies on a *view* abstraction generated by a special *synchronizer* primitive to drive the protocol. I will present a simple specification of a view synchronizer and its bounded-space implementation under partial synchrony. I will also explain how we applied our framework to produce the first rigorous liveness proof for the algorithmic core of the seminal PBFT protocol.

This is joint work with Manuel Bravo (Informal Systems) and Gregory Chockler (University of Surrey).

Please email for a Zoom link

Alexey Gotsman is an Associate Research Professor at the IMDEA Software Institute in Madrid, Spain, where he holds an ERC Starting Grant. Alexey obtained his PhD from the University of Cambridge in 2009. His research interests are at the intersection of distributed systems and formal verification.