Chess invariants
Skip to main content
Chess invariants
Get link
Other Apps
May 21, 2026
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.<br>It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.<br>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.
Invariants<br>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.<br>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.<br>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<br>These are predicates over a > 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.<br>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).<br>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?<br>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.<br>PieceCountNonIncreasing survives pawn promotion (when a pawn becomes a queen, the count is unchanged).
abstraction<br>tla
Get link
Other Apps
Comments
Anonymous said…
Did you use any of the verification tools (TLC, Apalache, TLAPS, ...) to deduce which of the invariants survive when we you added castling, pawns, en passant?
May 21, 2026 at 9:38 AM
Post a Comment
Popular posts from this blog
Hints for Distributed Systems Design
October 02, 2023
This is with apologies to Butler Lampson, who published the " Hints for computer system design " paper 40 years ago in SOSP'83. I don't claim to match that work of course. I just thought I could draft this post to organize my thinking about designing distributed systems and get feedback from others. I start with the same disclaimer Lampson gave. These hints are not novel, not foolproof recipes, not laws of design, not precisely formulated, and not always appropriate. They are just hints. They are context dependent, and some of them may be controversial. That being said, I have seen these hints successfully applied in distributed systems design throughout my 25 years in the field, starting from the theory of distributed systems (98-01), immersing into the practice of wireless sensor networks (01-11), and working on cloud computing systems both in the academia and industry ever since. These heuristic principles have been applied knowingly or unknowingly and has proven...
Read more >>
The Agentic Self: Parallels Between AI and Self-Improvement
January 02, 2026
2025 was the year of the agent. The goalposts for AGI shifted; we stopped asking AI to merely "talk" and demanded that it "act". As an outsider looking at the architecture of these new agents and agentic system, I noticed something strange. The engineering tricks used to make AI smarter felt oddly familiar. They read less like computer science and more like … self-help advice . The secret to agentic intelligence seems to lie in three very human habits: writing things down, talking to yourself, and...