Someone suggested that I model Redux in TLA+ and here we are. I spent about twenty minutes reading Redux tutorials and ran this by a few friends, so hopefully I didn’t misunderstand it too much. This post also uses a few more advanced TLA+ topics: if you are unfamiliar with TLA+, it should be mostly followable, but I’d recommend checking out my piece on deployments too, which is much simpler. Also, this is more about exploring modeling than convincing Redux people to use formal methods. Consider this more an example than a practical tutorial.