[j-pb]

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

[ahelwer]

It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.