FAQ
TLA+是什么？
TLA+ is a language for writing and checking “specifications”, or system designs. Once you have your specification, you can then test the specification directly for bugs, even before you’ve written any code. TLA+是一个编码和检查规约的语言，或系统设计语言。当你完成了规约后，就可以在写代码之前，测试规约是否有缺陷。
TLA+作者是谁？
Leslie Lamport, who’s also the man behind Byzantine fault tolerance, Paxos, and LaTeX. 是拜占庭容错算法、Paxos和LaTeX背后的男人：Leslie Lamport。
Fun fact: LaTeX is short for “Lamport’s TeX”! 热知识：LaTeX是“Lamport's TeX”的缩写。
PlusCal是什么？
PlusCal is a DSL that compiles down to TLA+. Most engineers find it an easier place to start than with pure TLA+, and it works great for a lot of specifications. The Core starts off with PlusCal (here's why) but fully teaches TLA+ by the end. I wrote topics and examples for both TLA+ and PlusCal. PlusCal是一个能够编译为TLA+的领域特定语言。非常多工程师都感觉使用PlusCal比直接用纯TLA+要更好入门一些，关键是在实现多数规约时基本够用。本教程的核心部分就是从PlusCal开始讲起（这里描述了为什么），不过最终还是完整介绍了TLA+。在教程的主题和例子中，同时包括了TLA+和PlusCal。
听说TLA+是一种“形式化方法”，这是什么东西？
“Formal methods” is, very roughly, the field of computer science dedicated to writing correct programs. This is usually done by first writing a rigorous mathematical definition of what “correct” means (“formal specification”), and then showing that the code satisfies that definition (“formal verification”). You can see what this process looks like in practice at Let’s Prove Leftpad, which is another project I run. “形式化方法”，粗略地讲，是计算机科学中用来保证写的程序是正确的领域。通常，起手是写一个严格数学定义，用以描述“正确”的定义（即“形式化规约”），然后展示一下满足上述数学定义的代码（即“形式化验证”）。关于这个过程，可以看一下作者的另外一个repo：Let’s Prove Leftpad。
You don’t see formal verification a lot because it’s really, really hard. There’s just too many complicated things in general-purpose code. One way to get around this is to focus on verifying a much simpler domain, like abstract designs. That’s what TLA+ does, making it easier to use at the cost of losing some power. 形式化验证很罕见的原因是，它非常非常难学。哪怕只是验证一段寻常的代码，也牵扯到很多复杂的概念。解决这一问题的方法之一，就是专注于验证一个更简单的领域，如抽象设计。这就是TLA+做的事情，使得形式化验证更容易被应用，不过与此同时，也丧失了一些形式化验证的其他特性。
TLA是什么的缩写？
“Three Letter Acronym.”（不是
Okay okay, it’s actually “Temporal Logic of Actions”. TLA+ is designed around the “core” of TLA. TLA+ users are a little shy about sharing the acronym because it intimidates beginners who’d otherwise have little trouble learning TLA+. 实际上是“Temporal Logic of Actions”，行为时态逻辑。
TLA+如何测试规约？
There are a few different tools that work with TLA+, but the main one is called TLC, which does model checking. That means it checker takes your specification and requirements, then checks every possible behavior of the spec against those requirements. 有一些工具能配合TLA+，不过最主要的一个是TLC，是做模型检测的。校验器读取规约和需求，根据需求校验规约中的所有可能的行为。
This gives much more thorough coverage than something like unit tests. Consider a system where three processes each do four sequential steps in parallel. There are 34,650 possible interleavings and 415,800 possible distinct states. TLC will check every single one. 这就比使用单元测试对代码的测试覆盖率高太多了。想象一下，一个系统中有三个进程，每个进程并行地执行连续的四个步骤，就会有34650种可能的交互操作，和41.58万种不同的状态。TLC可以检查每一种状态。
TLA+不能做什么？
The big one is that TLA+ tests designs, not code. There’s no built-in way to generate code from designs or check designs against code. This is in part because high level-designs are so much denser than code: a 50 line design could take thousands of lines of code to implement. TLA+只能测试设计，无法测试代码。内置的方法无法从设计生成代码，也无法根据设计检查代码是否正确。部分原因是高层设计比代码实现密集得多：50行的设计也许需要数千行的代码来实现。
(There are some techniques that help keep them in sync. I plan to write them up as a topic.) （还是有一些手段能够保持设计和代码的一致性的，本教程的主题部分会略有提及。）
TLA+ also can’t tell you if a design is good, practical, or even implementable, just whether it satisfies your requirements. It can help you in finding a good design, but you still need to put the work in. No tool can excuse us from being good engineers. TLA+也无法告诉你，你的设计是好是坏，是否实用，甚至能否实现为代码；它只能告诉你，你的设计能否满足你的需求。它能够辅助你找到一个好的设计，不过这不意味着你不需要自己努力了。要想称为优秀的工程师，还是要靠自强，不能依赖于任何工具。
所以TLA+真的找到bug了吗？
Yes! Here are just a few of the (public!) successful use cases: 确实能。这里有一些公开的成功实践的用户案例：
Espark Learning, an edtech company with just ten engineers, used TLA+ to find complex bugs in a distributed app installer, saving weeks of development and hundreds of thousands in revenue per year. (Disclaimer, I worked on this project. In fact it was how I started using TLA+!) 在Espark Learning项目中，TLA+帮助开发团队发现了安装程序中的一些bug，节省了大量的时间。（事实上，这个项目就是作者梦开始的地方。）
Amazon Web Services used TLA+ to model parts of S3 and DynamoDB, finding a 35-step bug that escaped all their tests and two code reviews.
Crowdstrike found multiple failure cases over just five days of workshops.
TLA+ has also been used by Azure, MongoDB, Confluent, Elastic, and Cockroach Labs to find bugs.
TLA+擅长什么？
TLA+ is great for modeling and finding bugs in concurrent and distributed systems. It’s also good for modeling systems that span more than one codebase. Something like an AWS Step Function involves multiple programs, services, and even human actors working together. All of these can be incorporated into a single system design and checked for errors. TLA+非常适用于给并发和分布式系统建模、发现bug。也适用于给跨代码仓库的系统建模。如AWS Step Function，这个系统包含了多个程序、服务，甚至需要多个人员协作。这一切，都可以设计进单一的系统，从而检查错误。
TLA+不擅长什么？
Like any tool, TLA+ has limitations. Aside from the obvious one (can’t test your code), there are some TLA+ weak spots:
Numerical code. TLA+ supports integers but not decimals or floating-point. TLA+支持整型，不支持小数和浮点数。
String manipulation. You can represent strings as a sequence of characters for basic manipulation, but it gets awkward. 字符串操作也不大行。
Probabilistic properties. You can say “X definitely happens” or “X never happens”, but not “X happens at least 90% of the time”. There are special tools for checking those kinds of properties. 没办法判断概率上的事情，不过有专门的工具干这个。
Reachability properties. You can’t say “it’s always possible for X to eventually happen, even if it doesn’t have to happen.” 大数定理整不了。
Realtime properties, like “If Y happens, X has to happen within five real actual seconds”. 实际时间的判断整不了。
There’s also some limitations to the current tooling. There’s not yet official features for interactive spec exploration or visualization.
使用TLA+需要很强的数学背景吗？
TLA+ does use a bit of math that’s not often used in regular programming, but it’s all learnable as you go. The Core gradually explains it as you go along. 该讲的在核心部分中都会讲到，学就完事了。
(If you want to know what to expect, the new math concepts are the boolean statement “X implies Y” and the set quantifiers “forall/some x in set”.)
是不是使用TLA+意味着不用写测试了？
Absolutely not. It only verifies the design is correct, not that the code is correct. Write your tests.
How does TLA+ compare to:
Unit Tests/Cucumber/TDD/PBT?
All of these act on code. You use them to check that you didn’t make a mistake writing the code. TLA+, by contrast, acts on designs. You use it to check that your design actually does what you want it to do.
Checking designs has an obvious drawback: you can make a mistake implementing your design. But checking designs also has some big benefits: you can make a design faster and test it more thoroughly than you can its implementation. Take “our microservices architecture never submits the same payment twice, even if services go down”. Testing that thoroughly would be a major undertaking. In TLA+ it’d be a couple-dozen lines.
Tradeoffs matter, and TLA+ is not “better than” testing. And if you’re not already testing, TLA+ isn’t the best investment.3 But if you’re already testing, then TLA+ is a fantastic addition to your toolbox.
SPARK/Idris/Dafny/Frama-C/F*?
These are all about formally verifying code; you can see examples of what they all look like at Let’s Prove Leftpad. As mentioned, formally verifying code is extremely difficult, which is why TLA+ focuses instead on verifying designs.
(Comparing “testing code” to “verifying code” is a whole ‘nother can of worms I can’t really get into here. I wrote a very rough overview here but it’s a few years out of date now.)
Alloy/Spin/Event-B/mCRL2?
Now we’re getting into the hard stuff. These are all other formal specification languages with the same domain as TLA+: verifying abstract designs instead of working code. They’re close enough for the subtle tradeoffs to matter. In my opinion, any comparisons of these tools needs to be be its own page, written by experts in both languages.
P?
I gotta be honest, I haven’t tried out P yet, so I have no idea how it compares to TLA+.
CTL*?
Dude if you know what CTL* is then you’re clearly just messing with me.
Last updated