TLA+ 架构
关于 TLA+ 的中文资料不多，英文资料却不少。
简单阅读就可以明白，TLA+ 用状态机和析取合取的顺序并发语义就实现了魔法一般的并发模型检查能力。
可魔鬼在细节中，使用说明书毕竟不是设计图，无法涵盖到我想了解的方方面面。比如
- 哪些操作是原子的？在 C++ 中，连简单的赋值语句都不一定是原子操作，那在 TLA+ 中呢，在 PlusCal 中呢？
- 状态遍历的时候是否会发生无限状态的可能？如果是的话怎么判断模型是否合法？这里想必是我知识上的疏漏，需要找到一两个关键词补全短板。
组件
当我们说 tla+ 的时候，我们是在指什么？
tla+ 实际由脚本式的 tlc 和交互式的 tlaps 两部分组成，前者的技术栈是 Java，后者是 OCaml。
我们平时使用的脚本、 VSCode 中的插件用的都是 tlc。 tlc 无法处理状态爆炸的问题，它的实际处理能力也只能覆盖 tla+ 的一个关键子集，对于涉及这个子集之外的问题会报错处理。 tlaps 可以交互式的剪枝，但是对形式化验证专业知识有较高的要求，不建议初学者使用。
TLC is a so-called "explicit-state" model checker that computes the state space generated by your specification and can then verify (safety and liveness) properties fully automatically. Its main constraint is state space explosion: the size of the state space grows exponentially with the number of processes etc., and this leads to a corresponding increase in verification time. There are a number of techniques to push back the frontiers of what TLC can handle effectively, including using symbolic constants, symmetry reduction etc., but the most important one is for you to decide how big you need your model to be to have enough confidence in correctness.
TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving.
As you say, there are symbolic model checkers that do not need to compute reachable states explicitly, and these are often based on SAT or SMT solvers. There is a project underway for designing and implementing a symbolic model checker for (a significant sublanguage of) TLA+, and I am sure it will be announced here when it becomes available for testing.