TLA+ 与形式化验证

这个话题有两份材料，建议按顺序读：

1. 从前端出发学 TLA+：状态、不变式、活性、公平与 SYMMETRY，共 13 节（第 1 到 13 课）。用按钮 loading、请求重试、两个标签页登录这三个前端场景，一步步讲清 TLC 在做什么，以及为什么 SYMMETRY 和 VIEW 会让“最终会发生”的检查出错。每个例子都在 2026-10-30 用真的 TLC 跑过。
2. pstack × TLA+ 深度学习包：FAQ、访谈提纲、自测题。原教程第 13 节说：“读完本教程再回去看会容易很多。”

学习路线

深度学习包里有一条 L0 到 L5 的学习路线，每一步带验收标准，见 学习路线与验收。

下载

• tla.zip：教程配套文件。每个 X.tla 配一个 .cfg，out-*.txt 是 2026-10-30 在 tla2tools v1.7.4 + Temurin 21 上的真实输出，run-all.sh 按顺序跑全部例子，pstack-PickWorker/ 复制自 pstack statechart 测试集。
• 压缩包不含 tla2tools.jar。请从官方 release 下载：tla2tools.jar v1.7.4，放进解压后的目录，再运行 sh run-all.sh。

来源

• Canvas「从前端出发学 TLA+：状态、不变式、活性、公平与 SYMMETRY」，2026-10-30 版本。
• Canvas「pstack × TLA+ 深度学习包」，2026-10-30 版本。
• tla-tutorial.zip，2026-10-30。