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协议、分布式事务 等相关算法的验证,点我进入项目

# 其他资源