Chess Invariants

# Chess invariants Source: [http://muratbuffalo.blogspot.com/2026/05/chess-invariants.html](http://muratbuffalo.blogspot.com/2026/05/chess-invariants.html) 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\. [](https://blogger.googleusercontent.com/img/a/AVvXsEieheth329KZWFID8TgPUYxsXcddqVnJITtNzlQdKl_6ZijHM5eabj9Os0AuYsihkAkjrVy9ECIofotAr7MQWx8lI5BDbr8lbvhcMI7PdEmyYsFS8LerDsx00AOJTRBMCSo6ZoVLlOylVRhtB6Xo-bQSgkzSzkufGMjpNfPiKHLfHmfGN7DCCp_IlE-1Go) 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\. [](https://blogger.googleusercontent.com/img/a/AVvXsEikc32YDNgo2Ye1s9hJkkEE6xBVjHigF4Sv0I32t1TDwY-vrujJsaM70yEfiS49vhI2iJ-snRAxHAfz0_Qlgu_9x-0ivqIfMBFn0Z6KSsp9y3CWOuUfjwufV8oNc-Pj65phWy_KTTPIbYGkyYuZjr1UlpD0Wyu-9xi9PEmyADPzbxDyLPMHB5LxrQQgNd4) 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\. In the case of a system like chess, I think the transition invariants come in very handy as you may see below\. ## State invariants [](https://blogger.googleusercontent.com/img/a/AVvXsEhsJ4jS2lpTvflFJHGDMZcIFa81Ew3h3_HczmPIVV-rS6CIcSI07Wd-B0MpfBCKtQ8OzXsrgDzxzFCHEcNhK1HMleycrfyF_RuLaMIXt1XACUu81HuE610Z7Zb1YutnR5_usJtNHXzQNjT4jv37YbCWvd_MZlAeS6KAAkOOU0CxVg70bI1qHpnnCXX6FOI) TypeOKsays every variable lives in the right space\. It is boring, but it has caught more bugs than I would like to admit\.OneKingPerColorandBothKingsOnBoardare also sanity checks\. TurnParity is the first interesting one\. It ties two state variables together:WHITEmoves on even moves,BLACKon odd\. TheMakeMoveaction satisfies thisTurnParity\. PreviousPlayerNotInCheckrestates the rule that "you must end your turn not in check" as "look back: the player who just moved is not in check"\.NotBothInCheckis 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:xis the value of the variablexin thisstate, andx'denotes the value in thenext\-state\. [](https://blogger.googleusercontent.com/img/a/AVvXsEhY9j3UHT8v9oALhxmfy6Mv2w-I2pcfQqm5yY3pWly5y4tws1vtVKrd9VFEWZulo5Fv-hhOW2l7jnis6Lmwa1a5N90NXZR526gPwQyrZenA_y-SsHgaZK67nDks3cYANLj61hanmhB2aMB679x20ubks06NsDaD6x-PkB0KKOyQ-xvkWqFwiCsiCaMVV2M) MoveCountStrictlyIncreasesandTurnAlternatessay each step increments the move count with the colors flipping\. If a transition ever messes this up, something has gone wrong\. PieceCountNonIncreasingrules out pieces appearing out of thin air\.SingleCapturePerMovetightens this: at most one piece disappears per step\.ExactlyTwoSquaresChangeis 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? ExactlyTwoSquaresChangegets 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\. PieceCountNonIncreasingsurvives pawn promotion \(when a pawn becomes a queen, the count is unchanged\)\. **UPDATE**:[James Corey writes](https://mastodon.acm.org/@jaymcor/116613347381723112): As always, enumerating the rules gets you thinking even pre analysis\. Like, apparently it wasn't until 19th century that people made clear that you couldn't promote a pawn to a King, surprising an attempted checkmate by responding Le roi est mort, vive le roi\!