diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md
index e466e4e0da..7f6ce09c4b 100644
--- a/docs/src/apalache/tuning.md
+++ b/docs/src/apalache/tuning.md
@@ -64,7 +64,7 @@ Note that there is no direct correspondence between the transition numbers and
 the actions in the TLA+ spec. To find the numbers, run Apalache with
 `--write-intermediate=true` and check the transition numbers in
 `_apalache-out/<MySpec>.tla/*/intermediate/XX_OutTransitionFinderPass.tla`: the
-0th transition is called `Next_si_0000`, 1st transition is called
+0th transition is called `Next_si_0000`, the 1st transition is called
 `Next_si_0001`, etc.
 
 ### Invariant filter
@@ -83,6 +83,14 @@ model checker to check
 
 [Trace invariants][] are checked regardless of this filter.
 
+Note that there is no direct correspondence between invariant numbers and the
+operators in a TLA+ spec. To find the numbers, run Apalache with
+`--write-intermediate=true` and check the invariant numbers in
+`_apalache-out/<MySpec>.tla/*/intermediate/XX_OutVCGen.tla`. The 0th state
+invariant is called `VCInv_si_0`, the 1st state invariant is called
+`VCInv_si_1`, and so on. For action invariants, the declarations are named
+`VCActionInv_si_0`, `VCActionInv_si_1` etc.
+
 This option is useful, e.g., for checking consensus algorithms,
 where the decision cannot be revoked. So instead of checking the invariant
 after each step, we can do that after the algorithm has made a good number of