This is a neat example of refinement, and will become even better after the future blog post on a system further refining/implementing this property. I wonder about model-checking performance, because looking at your initial state:

Orderings(S) ≜ {
  seq ∈ [1 ‥ Cardinality(S) → S] :
    ∀ i, j ∈ DOMAIN seq :
      seq[i] = seq[j] ⇒ i = j
}

Init ≜
  ∧ fate ∈ [Tr → {Committed, Aborted}]
  ∧ to ∈ Orderings(CT)
  ∧ benv ∈ [1 ‥ N + 1 → [Obj → Val]]

The initial state space seems enormous! Assuming Tr, CT, Obj, and Val are all constant sets and N is a constant natural number, this scales as (where |S| is used to denote cardinality):

(2^|Tr|) * |CT|! * (|Val|^|Obj|)^N

which is a pretty astonishing rate of growth. At that point I would probably give up on using the TLC finite model checker and reach for the Apalache symbolic model checker.

I’ve long dreamed of making something like the Complexity Zoo but for consistency, with TLA+ as the base formalization. Aphyr already made this site but it doesn’t present the formalizations in a formal language. This spec would be a good start to it!