TLA+ 资源汇总
This is the home page of the TLA+ web site. TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code. The following are the top-level pages of the web site.
TLA 是 Paxos 算法的发明者 lamport 创建的一门形式语言，用于描述并发程序和检查其正确性。
TLA+ 是 TLA 的程序语言版本。
官网
如果英文听读没障碍，最好的教材就是官网，文档、视频等资源非常丰富，下面介绍的很多资源也出自这里。
《Specifying Systems》
出自 lamport 的全面介绍 TLA+ 的书籍，全书分为四个部分 - 第1章 - 第7章，写规约（specification）时必须了解的内容 - 第8章 - 第11章，介绍了规约中的时序逻辑 - 第12章 - 第14章，语法分析器、TLATEX排版程序、TLC模型检查器 - 第15章 - 第18章，TLA 语言参考手册
点击下载地址下载本书 pdf，重要章节有对应中文翻译《Specifying Systems》中文版。
PingCAP 的课程分享
视频建议 1.5 倍速食用
原文中的 PPT 链接错误，点这里下载
- TLA+ 是什么？
- 为什么要用 TLA+ ？验证设计的正确性
- Safety Property 和 Liveness Property
- 一个求最大公约数的例子
- 检验 Percolator
- 检验 Multi-Raft Region Merge
tlaplus 的应用
tlaplus 的 examples 项目中有很多算法的 TLA+ 描述，比如 Paxos 和 Raft，点我进入项目
pingcap 的应用
包括 Raft、Percolator协议、分布式事务 等相关算法的验证，点我进入项目