学习 TLA+ (Homepage: https://lamport.azurewebsites.net/tla/tla.html) 有助于设计、理解以及证明分布式算法。
初学资料可以参考：https://lamport.azurewebsites.net/tla/learning.html，
- 先从 TLA+ Video Course 入手
- 配合阅读 The TLA+ Hyperbook
入门之后，可以阅读相关论文 (https://lamport.azurewebsites.net/tla/papers.html?back-link=more-stuff.html#papers?unhideBut@EQhide-papers@AMPunhideDiv@EQpapers), 比如
- Introduction to TLA; 1994
- The Specification Language TLA+; 2008
- The Temporal Logic of Actions; 1994
- Model Checking TLA+ Specifications; 1999
强烈推荐的系列博客 (Video: TLA+ in Practice and Theory (pressron)):
- Part 1: The Principles of TLA+
- Part 2: The + in TLA+
- Part 3: The (Temporal) Logic of Actions
- Part 4: Order in TLA+
最终希望能读懂论文：
- Hiding, Refinement, and Auxiliary Variables; 2019
- Auxiliary Variables in TLA+; 2017
- Prophecy Made Simple; 2020
另外，使用 TLA+ Toolbox 的过程中，可以随时记录“有哪些功能可以改进、需要添加”等想法。