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+