简介：

https://en.wikipedia.org/wiki/TLA%2B

 

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.

 

 

目标：

初阶目标：检验状态机的合理性。

高阶目标：设计无漏洞的系统和算法。