Modeling Redux with TLA+

1 · Hillel Wayne · Feb. 12, 2018, midnight
Update 01/07/19 Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definitely isn’t refinement. mkay thanks! Someone suggested that I model Redux in TLA+ and here we are....