I find this to be an almost everpresent problem in my own TLA+ specs, and generally resort to a similar solution. It's ugly and annoying when the counter values end up in many places in your specification -- garbage collection becomes quite complex. (Perhaps a level of indirection, along with reference counting, might help here.)
I've always felt this is a great candidate for a new built-in TLA+ "ordered opaque value" type. I know though that symmetry clauses can mess with checking temporal properties, and I haven't had time to think through whether there would be similar issues with such a built in type.
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