It's absolutely bonkers that TLA+ struggles with this, given that a system is eventually consistent IFF it is logically monotonic (CALM) [1]. This also doesn't

It's absolutely bonkers that TLA+ struggles with this, given that a system is eventually consistent IFF it is logically monotonic (CALM) [1]. This also doesn't make intuitive sense to me. Model checking should be easier for monotonic models, because because the total model check can be viewed as a consistent sum of all partial checks. I've collaborated on a monotonic parser once, which was essentially a monotonic logic programming language. One of the key insights was that you can replace backtracking search of the state space with solving a set covering problem where you attempt to find the union of all sub-parses that cover the sentence fully. So for monotonic systems you should be able to dynamically program / divide and conquer the heck out of it. 1. https://arxiv.org/abs/1901.01930 https://arxiv.org/abs/1901.01930