TLA+ 笔记

很久以前学过一些 Prolog,当时主要是为了学习人工智能和数理逻辑。TLA+ 与之有一点点像,Prolog 可以用来处理各种规划问题、一阶逻辑推理,TLA+ 可以用来设计各种分布式、异步系统,搭配 TLC(model checker) 来做验证——他们的设计目标都不是解决通用的编程问题,而是通过数理逻辑解决一些特定领域问题。 TLA+ Tools 包含很多工具,可以在这里下载,大部分人都是使用这个 Tools: http://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html 在里面的链接指向的 github 地址里,有 Windows、Linux、Mac 的二进制版本,良心。 在看 TLA+ Community Meeting 2018 的时候还看到了一个形式验证语言(其实是 Python 的扩展)DistAlgo,整体思路和 Demo 看起来特别棒,就是目前各种材料和介绍还是相对少,所以我没有继续研究下去,有兴趣和时间的话,看看 DistAlgo 也挺好。 下面是笔记。 介绍 分布式系统的正确性特别难验证,所以做出了 TLA+,因为 2015 年 AWS 在 CACM 发了一篇 How Amazon Web Services Uses Formal Methods 引起了很多人注意,年底 TLA+ 作者之一的 Langworthy 和 Lamport 找微软高层推动 TLA+ […]