Two Bugs in the SAFE Predicate: Finding and Formally Verifying Liveness Failures in Byzantine Lattice Agreement

We have modeled the Byzantine Generalized Lattice Agreement algorithm in Quint and found two bugs in the SAFE predicate