The formula is true of all behaviors (sequences of states) such that Init is true in the initial state and Next \/ board'=board is true of all pairs of subsequent states. For the definition \A move \in ... : EnvNext(move), TLC attempts to construct a successor state such that the formula EnvNext holds for all values in the set, and this is certainly not what you intend. Formally,
board' = Append(board, move)
would have to hold simultaneously for all values move \in Move, as well as board' = board (because of the clause for Pass), and this is impossible. Therefore TLC cannot construct any successor state (except stuttering) for the initial state and signals a deadlock.
When you replace \A by \E, TLC will construct one successor state per move, as well as the (stuttering) successor for Pass. In this way, you obtain the tree (or in general, graph) of reachable states. Every branch of this tree corresponds to a possible behavior satisfying your spec, and TLC will evaluate the properties over each branch.
Note by the way that the transition for Pass is an explicit stuttering step according to your definitions, indistinguishable from the implicit stuttering transition that is anyway possible for TLA+ specifications.
Regards,
Stephan