# 简介

{% hint style="info" %}
翻译自：<https://learntla.com/>
{% endhint %}

{% hint style="success" %}
**Note**

Welcome to Learn TLA+! This is still a work in progress, please see [What’s New](https://learntla.com/whatsnew.html) for updates and please raise any questions or concerns at the [github repo](https://github.com/hwayne/learntla-v2). I’d love to hear your feedback!\
欢迎来到**学习TLA+**！该教程目前还在逐步完善中，访问[最近更新](/whats-new.md)页面查看教程更新日志；有任何问题或建议，移步该教程的[github仓库](https://github.com/hwayne/learntla-v2)提issue。\
（对中文翻译有任何改进建议，请联系<eancuznaivy@gmail.com>）

(In the meantime, you can find the old version at [old.learntla.com](https://old.learntla.com/).)\
老版本：[old.learntla.com](https://old.learntla.com/)。
{% endhint %}

## 学习TLA+

Most software flaws come from one of two places. A code bug is when the code doesn’t match our design— for example, an off-by-one error, or a null dereference. We have lots of techniques for finding code bugs. But what about design flaws? When it comes to bugs in our designs, we’re just taught to “think about it really hard”.\
大多数软件缺陷，是由两个原因之一造成的。其一是编码错误，即**代码与设计不符**：如off-by-one错误或解引用空指针。如今有很多手段辅助我们发现编码错误（静态分析等）。另一个就是**设计缺陷**了。然而，面对设计缺陷，我们常常只能做到“使劲想想”。

TLA+ is a “formal specification language”, a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and Crowdstrike. TLA+ doesn’t replace our engineering skill but *augments* it. With TLA+ we can design systems faster and more confidently. Check out the [Conceptual Overview](https://learntla.com/intro/conceptual-overview.html#chapter-overview) to see an example of this in practice.\
TLA+是一个“形式化验证语言”，是在完成系统设计之后，**直接验证设计是否正确**的手段。TLA+由图灵奖获得者Leslie Lamport开发，目前已经被多个大厂实践。TLA+并非用于代替工程技能，只是起到增强作用。利用TLA+，我们可以更快地完成系统设计，并对系统的质量更有把握。[概念概述](/conceptual-overview.md)中包含更多实践上的例子。

### 关于本教程

This is a free online resource for learning TLA+. To help both beginners and experienced users, the guide is divided into three parts:\
这是一个学习TLA+的免费在线资源。为了对初学者和有经验的老手都能够起到帮助作用，本教程分为三部分：

* The [Core](https://learntla.com/core/index.html): a linear introduction to all of the TLA+ language. It starts with basic operators and gradually progresses all the way to advanced topics. The core is intended to be read **linearly**: people new to TLA+ should start with the conceptual overview and then work forward from there. People comfortable with TLA+ should skim until they find new material.\
  [核心](/tlaplus/core.md)：这部分是关于TLA+语言所有信息的直白（线性）的介绍。从基本的操作符开始，一直过渡到高阶的话题。对于TLA+新手，可以从概念概述开始，按顺序读完核心部分。对于TLA+老手，也可以按顺序略读这一部分，直到遇到不熟悉的内容。
* [Topics](https://learntla.com/topics/index.html): “Optional” advanced material. Any individual lesson will be useful to *many* but not *all* TLA+ users. Unlike the core, these are designed to be mostly independent of each other. If topics have dependencies on other topics, I will call them out.\
  主题：“可选的”高阶教程。每一个章节都应该能对大多数TLA+使用者提供帮助，不过并不是所有TLA+使用者都能用得上。不同于核心部分，这一部分地不同章节基本上互相独立。如果不同章节之间存在依赖，教程中会给出相应提示。
* [Examples](https://learntla.com/examples/index.html): Applications of TLA+ to specs, showing both how to write and understand specs.\
  示例：TLA+的在规约上的应用，呈现如何书写和理解规约。

This guide is still under development, check [What’s New](https://learntla.com/whatsnew.html) to see most recent updates and the [roadmap](https://learntla.com/whatsnew.html#roadmap) to see what I’m currently working on.

### 关于作者

I’m Hillel. I’m part of the TLA+ foundation and the author of the book [Practical TLA+](https://www.amazon.com/Practical-TLA-Planning-Driven-Development/dp/1484238281). I wrote this because I want TLA+ to be as accessible as possible and didn’t like that my book cost money. I have a [blog](https://www.hillelwayne.com/), a [twitter](https://twitter.com/hillelogram/), and a [weekly newsletter](https://buttondown.email/hillelwayne/).\
作者Hilel，TLA+基金会的一员，《Practial TLA+》的作者。该教程旨在推广TLA+，且读起来不花钱。作者同时维护有博客、推特和周报。

(Full disclosure, I’m also a [professional TLA+ consultant](https://hillelwayne.com/consulting/) and \<plug>run workshops\</plug>.)


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://learntla.eanzhao.com/intro.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.