把国际象棋写成 TLA+ 模型：不变量暴露的不是棋术，而是规则边界

Murat Demirbas 在 5 月 21 日的《Chess invariants》里，做了一件有点反常的事：他没有从棋术讲国际象棋，而是把它当成一个形式化系统。

白方走一步，黑方走一步。棋盘从一个状态跳到下一个状态。换成 TLA+ 的语言，这更像两个进程在交错执行，而不是一篇普通的棋类规则介绍。

我更在意的是这件事背后的训练价值：不变量不是用来判断谁会赢，而是用来逼问模型有没有撒谎。哪些条件真的恒成立，哪些只是为了写模型方便，特殊规则一来就能看出来。

国际象棋在这里是轮流执行的系统

Demirbas 的抽象很清楚：国际象棋可以被看成白黑双方交替执行动作的状态机。

系统状态至少包括棋盘、当前回合、步数、棋子位置等变量。每一步走子，都是一次状态转移。这里的重点不是“马走日、象走斜线”，而是状态能不能保持合法。

这也是它和普通棋规文章的区别。棋规文章关心某个棋子怎么走；形式化建模关心的是：任何合法状态下，哪些条件必须为真。

比如状态不变量可以包括这些东西：

这些检查不关心局面优劣。它们只回答一个问题：这个状态像不像一个真实棋局可能到达的状态。

对做分布式系统的人，这个问题很熟。Raft 里不能同时出现两个合法 leader，账户系统里余额不能凭空增加，权限系统里用户不能绕过授权拿到能力。棋盘只是换了一张皮。

状态不变量看局面，转移不变量看动作

文章里更有用的分法，是把不变量拆成两类。

状态不变量只看一个局面。转移不变量看的是一次动作前后，也就是当前状态和下一状态之间的关系。在 TLA+ 里，很多关键问题都藏在 x 和 x' 之间。

基础模型里，转移不变量可以包括：步数递增、回合交替、棋子数量不增加、单步最多吃一子，以及每步只改变两个格子。

这几条听上去都很朴素，但它们比“棋盘当前是否合法”更容易抓住建模错误。

如果写成规格，味道大概会接近这种关系：turn' = Other(turn)，moveNo' = moveNo + 1，PieceCount(board') <= PieceCount(board)。这不是说原文已经完成工具验证，而是说明读这类文章时该盯哪里。

很多工程 bug 也不在静态截图里。它们发生在状态变化的一瞬间。

一次重试有没有重复扣款？一次 leader 切换有没有短暂双主？一次权限变更有没有留下旧 token？这些问题都不是“当前状态看起来对不对”能完全回答的。

棋局的好处是足够小。读者能在熟悉场景里看见形式化方法的锋利处。

特殊规则会专门打穿漂亮假设

Demirbas 也没有把这个模型说成完整覆盖国际象棋规则。基础模型就是基础模型。真正有意思的地方，是王车易位、吃过路兵、兵升变这些特殊规则会怎么检验不变量。

王车易位最直接。王和车同时移动，一步会影响四个格子。于是“每步只变两个格子”这条基础约束就不再成立。

吃过路兵更别扭。走子的兵落在一个目标格，被吃掉的兵却不在这个目标格上。一次动作至少涉及三个格子。它会提醒建模者：如果把“吃子一定发生在目标格”写死，模型就已经偏离规则。

兵升变击中的不是数量，而是类型。棋子数量不增加仍然可以成立，但“同一枚棋子永远保持同一类型”就不能当不变量。

这类地方很像工程里的兼容逻辑。主流程看起来干净，边界条件一接进来，原先顺手写下的约束就开始露馅。差之毫厘，谬以千里。

对两类读者，行动也不一样。

做分布式系统和形式化方法的人，可以把这篇文章当成一次规格审查练习：不要只列安全性质，还要列动作前后的约束；遇到例外流程，要检查是不变量错了，还是动作需要拆分。

对想上手 TLA+ 的软件工程师，更现实的做法不是直接追求完整证明，而是先挑一个小系统写三件事：状态变量、状态不变量、转移不变量。等基础规则跑通，再把“特殊规则”单独建成动作。这样成本低，也更容易发现自己把假设写成了事实。

目前看不清的是工具层面的结果。原文没有声称已经用 TLC、Apalache 或 TLAPS 完成验证，评论区只是有人问到这些工具。所以读这篇文章时，不该把它当成验证报告。

更该看的变量是：这些不变量进入可执行规格后，哪些要弱化，哪些要按动作分类，哪些必须被特殊规则重写。这个问题，比“国际象棋能不能被形式化”更贴近工程现场。