Hi Gregory,
the spec passes because of the changes in steps v12 and v13. In preparation of step v17, step v16 uses TLC to validate our inductive invariant "candidate" IInv by model-checking IInv /\ [Next]_vars => IInv'. In step v17, we prove that the spec is deadlock-free with TLAPS. The first page of Lamport's "Using TLC to Check Inductive Invariance" [1] explains the validation of inductive invariants in detail.
Markus
PS: With the necessary type annotations [2], Apalache should validate IInv for larger values of Producers, Consumers, and BufCapacity.