主要观点：很多正式规范项目涉及并发或分布式系统，人们常认为并发难是因为人类线性思考而不擅长并发推理，但作者认为是状态空间爆炸导致并发难，具体如下：

• 行为、交错和不确定性：多个执行线性序列步骤的代理，不同代理算法不同，不同交错会导致不同行为和状态，状态空间增长快，复杂并发系统状态数可达数百万甚至数千万。
• 缩小状态空间：使并发更易的方法首要在于管理状态空间，如线程共享内存易导致状态空间大，可通过互斥锁等修剪，改用内存隔离进程可减少交错，低级别原子指令、数据库事务等也可减少状态空间，语言构造也能更好地修剪状态空间。
• 限制：状态空间小通常较好，但要考虑空间拓扑，不同形式的不确定性也有影响，一些高级范式会导致特定状态空间拓扑，还有 bug 状态和行为的区别，活锁更难推理。
  视频 appearance：作者在 David Giard 的 Technology and Friends 节目中谈论 TLA+，可查看相关视频。
  脚注说明：
• 代理指并发参与者，如线程、进程等，并发文献常用“进程”但易与操作系统进程冲突。
• 若写操作非原子性，可能出现数据竞争，变量赋值可能在一行中包含多个步骤。
• 是否有研究将状态空间中的异常子图与可能的 bug 相关联？