Chess Invariants

This article applies formal verification techniques to chess by modeling the game as a concurrent system and identifying key invariants—safety properties that must always hold true. The author categorizes invariants into state invariants (predicates about individual states, like "both kings must be on board") and transition invariants (predicates about state changes, like "exactly two squares change per move"), demonstrating how these invariants break down when complex rules like castling or en passant are added. The exercise illustrates how rigorous rule enumeration reveals the nuances of chess mechanics and helps catch logical inconsistencies in system design.