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