Chess invariants

A blog post exploring chess through the lens of formal methods and distributed systems thinking. The author models chess as a concurrent system with interleaved execution (turn-taking) and derives both state invariants (TypeOK, OneKingPerColor, TurnParity, PreviousPlayerNotInCheck) and transition invariants (MoveCountStrictlyIncreases, PieceCountNonIncreasing, ExactlyTwoSquaresChange). The post then examines which invariants break when advanced rules like castling and en passant are introduced, using chess as a vehicle to illustrate how invariant reasoning works in system design.