TLA+是Lamport大神近年来着力研究和推广的形式化描述语言，TLC Model Checker则是相应的形式化验证工具。
Lamport是图灵奖获得者，早期著名的贡献包括Latex和Paxos等等等等。无需赘述。
顺便说下，Lamport写的东西，大部分都不容易懂。比如Paxos当年就以难于理解著称，以至于有后来有很多文章专门去解释它，包括Lamport自己写的"Paxos Made Simple"，大家仍然觉得看不懂，Raft的Paper的一个出发点后也是Paxos的难懂。
TLA+相当抽象难懂，但是难懂的不在语言本身，而是数学思维方式。我本人也在不断学习中。想系统地介绍TLA+并让文档易于理解是个非常艰难的工作，因为它本身就比较偏理论。
这个系列的文档将是个长期的业余工作，但是相信能够帮助大家解决一些复杂的问题。比如，设计了一个分布式系统或者并发算法后，即使运行了一段时间没发现问题，也不能确定真的没有Bug，是否所有的场景都测试到了。在这种情况下，用TLA+去描述算法，再用TLC Model Checker去做验证，就是非常有意义的。
按照数学模型去思考，有几个好处：
- 抽象、关注本质. Lamport自己在一个视频中说，Paxos的TLA+ spec分为三个模块，Consensue => Voting => Paxos，实际上大致体现了他当时思考Paxos算法的过程(虽然那时候没有TLA+)。不断思考本质问题和抽象，而不是一开始就考虑实现细节。用数学模型去描述，我们更清楚知道模型的目标是什么，需要保证什么。
- 简明、准确。用自然语言或者描述算法，不同的人会产生不同的理解 ，它本身不是一个准确的工具。即使伪代码也没有数学准确。而且伪代码没有统一标准。
- 可验证。使用TLA+描述语言去描述核心算法或者模型后，可以使用工具去检查算法的正确性。
我会用部分篇幅介绍TLA+ 语言和工具本身，但是大家不要把语言看作重点，重点是用数学思维去思考问题，去验证自己的思维，并且应该是在实施系统开发之前。这些会在分析一些例子时慢慢体会。
如果阅读或者实践中遇到问题，欢迎提问，以便于完善。
