Byzantine consensus protocols are designed to build resilient systems to achieve consensus under Byzantine settings, maintaining safety guarantees under any network synchrony model and providing liveness in partially or fully synchronous networks.
However, several Byzantine consensus protocols have been shown to violate liveness properties under certain scenarios. Existing testing methods for checking the liveness of consensus protocols check for time-bounded liveness violations, which generate a large number of false positives.

In this thesis, for the first time, we check the liveness of Byzantine consensus protocols by the temperature and lasso detection methods and precisely detail ad-hoc system state abstractions that should be used to test these algorithms.
We provide a theoretical analysis of the recently-published safety and liveness attacks and whether the existing test method is able to detect them.
To investigate the issues, we focus on the streamlined blockchain consensus, particularly the HotStuff protocol family, which has been recently developed for blockchain consensus. Among these protocols, the HotStuff protocol itself is both safe and live under the partial synchrony assumption, whereas 2-Phase Hotstuff and Sync HotStuff protocols can violate liveness in subtle fault scenarios.
We implemented our liveness checking methods on top of the Twins automated unit test generator to test the HotStuff protocol family and explored the scenarios with message delay.
Our results indicate that our methods successfully detect all known liveness violations and produce fewer false positives than the bounded liveness checks.