A colleague that I met in a regional tech community, Hillel Wayne, recently solicited some feedback on the Redux portions of this informative piece on using TLA+ to model Redux. I obliged him, and learned a lot about TLA+ in the process!

It's worth a read:

Modeling Redux with TLA+