简介：
https://learntla.com/introduction/
https://en.wikipedia.org/wiki/TLA%2B
http://www.top100summit.com/think/12702
https://www.jianshu.com/p/7ae049ce4a82
| TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint. |
| A specification language is a formal language in computer science used during systems analysis, requirements analysis and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system. |
目标：
初阶目标：检验状态机的合理性。
高阶目标：设计无漏洞的系统和算法。
转播
