invariants

本文将国际象棋建模为并发系统，并推导出状态和转换不变量，展示了使用TLA+的形式化验证技术。

文章认为，结构性反压（例如编译器、类型检查器）比改进AI模型更能确保代码正确性，并介绍了Shen-Backpressure作为一种实现该方法的工具。

探讨软件系统中非法状态与不期望状态的区别，认为不期望状态有时是必要的，必须显式建模。