This repository contains two PlusCal/TLA+ models of the Streamlet blockchain-consensus algorithm. The repository also contains setup files for the TLA+ Toolbox (so if you import the specifications in the toolbox everything should be ready to run the TLC model-checker).
The specifications are described in the following blog post: https://www.losa.fr/blog/streamlet-in-tla+