A readable and computable formalization of the Streamlet consensus protocol

Consensus protocols are the fundamental building block of blockchain technology. Hence, correctness of the consensus protocol is essential for the construction of a reliable system. In the past few years, we saw the introduction of a myriad of new protocols of the BFT family of consensus protocols. The Streamlet protocol is one of these new protocols, which while not the fastest, it is certainly the simplest one.

In order to have strong guarantees for the protocol and its implementations we want to obtain formalizations that are readable enough to be used to communicate between formalizers and implementors, that have a mechanized proof of correctness and that can support the testing of implementations.

We present a readable and computable formalization of the Streamlet protocol in Agda, providea mechanization of its proof of consistency, and show how one may use the formalization for testing implementations of it.