Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.

It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.

You know what we do with concurrent systems here? Here we model them, and we distill their invariants.

Here is some setup definitions first.

In a CS or math paper, if you write "Section 2: Model and Problem" well enough, the rest of the paper writes itself. With this setup you can sort of see what the actions will be.

In fact, forget about the actions. Let's look at some invariants.

When deriving invariants we ask: what must always be true? I find it useful to split the safety invariants into two camps: state invariants (which are predicates over a single state) and transition invariants (which are predicates over a step). The transition invariants are not as commonly used as state invariants, but they can be very helpful, especially when you are reasoning about transitions of a system.

State invariants

TypeOK says every variable lives in the right space. It is boring, but it has caught more bugs than I would like to admit. OneKingPerColor and BothKingsOnBoard are also sanity checks. 

TurnParity is the first interesting one. It ties two state variables together: WHITE moves on even moves, BLACK on odd. The MakeMove action satisfies this TurnParity.

PreviousPlayerNotInCheck restates the rule that "you must end your turn not in check" as "look back: the player who just moved is not in check". NotBothInCheck is a corollary.

Transition invariants

These are predicates over a <<state, next-state>> pair, written with the bracketed form: [][P]_vars. They express how things change with constraints.  The notation is simple: x is the value of the variable x in this state, and x' denotes the value in the next-state.

MoveCountStrictlyIncreases and TurnAlternates say each step increments the move count with the colors flipping. If a transition ever messes this up, something has gone wrong.

PieceCountNonIncreasing rules out pieces appearing out of thin air. SingleCapturePerMove tightens this: at most one piece disappears per step. ExactlyTwoSquaresChange is the strongest here. It says precisely two squares change per move, the source (now empty) and the destination (now holding the moving piece). 

Haha, yes, this is a model of the basic chess rules only. A useful exercise here is to consider which of these invariants survive when we add castling, pawns, en passant?

ExactlyTwoSquaresChange gets violated when we add castling: four squares change in one move. Similarly, en passant captures a piece not on the destination square, so three squares change.

PieceCountNonIncreasing survives pawn promotion (when a pawn becomes a queen, the count is unchanged).