but what is meant as state here is not exactly what is meant as mutable state in programming. Here's an example of a (pure) Haskell function:
gcd :: Int -> Int -> Int
gcd x y = if x == y then x
else if x > y then gcd (x - y) y
else gcd x (y - x)
there is no mutation going on, yet the variables x and y are variables whose values change over time (at each iterative step). It's true that there may not be any mutation of memory addresses (actually, there likely is, because the function is tail-recursive), there is still state. The corresponding TLA+ specification also says nothing about mutation of memory cells. In fact, TLA+ has no notion of memory at all, unless you choose to model it. Variables whose values can change just means that a set of names refers to different values -- this happens in pure functional languages all the time.