TLA+是分布式领域大名鼎鼎的Turing 获得者 Leslie Lamport 发明的针对数字系统（算法，程序，计算机系统）的一种high-level 建模语言。TLA+专门为并行和分布式系统所设计，high-level意味着在代码之上的更高的设计抽象，在我们正式开始写下第一行代码之前，TLA+就可以帮助我们设计并验证一个复杂系统。
简单来讲，TLA+的任务用严格的数学语言去刻画（specify）一个系统中可能允许的所有行为，即，它在一次执行过程中所有可能达到的状态。TLA+没有办法直接帮我们产出任何一句有实际生产意义的代码，但它给我们提供了一个新的思考方式和设计工具，学习和理解 TLA+ ,无疑可以帮助你成为一个更好的编程者和工程师。
本系列博客可以看作TLA+的学习心笔记和心得，主要学习资料为The TLA+ Video Course和《Specifying Systems》。