AI与形式验证的讨论，TLA+应用案例
有一种流行的理论认为，人工智能最终将使形式验证成为主流，因为当机器编写大部分或全部代码时，需要数学证明正确性。但这会发生吗？Hillel Wayne 是最佳回答者之一。时间戳：
00:00 介绍
04:32 Crossover 项目
11:37 软件工程做得更好的地方
15:30 传统工程做得更好的地方
18:17 形式方法
29:32 TLA+：它是什么及演示
36:58 亚马逊的 TLA+
38:10 分布式系统失效的方式
41:03 形式方法与系统思维
46:20 学习数学的价值
50:23 TLA+ 的适用与不适用
52:50 Alloy：一种用于软件建模的声明式语言
58:53 其他形式方法工具
1:01:24 基于属性的测试
1:05:31 人工智能与形式验证的需求
1:12:29 程序员的逻辑
1:14:35 Hillel 对 2025 年人工智能影响的预测
1:21:30 书籍推荐
由以下机构提供：
• @AntithesisHQ – 无需人工审查或传统集成测试即可验证系统正确性，避免错误或中断。 https://t.co/AKYm4cctss
• @turbopuffer – 基于对象存储的向量和全文搜索引擎。快速、廉价且极具可扩展性。 https://t.co/w9y67GsFZJ
• @WorkOS – 让你的应用企业级就绪所需的一切。 https://t.co/aiAee0pcUP
与 Hillel 交谈时，我发现两件特别有趣的事情：
1. 亚马逊使用 TLA+ 发现了一个几乎无法通过形式方法找出的错误。
在论文《亚马逊如何使用形式方法》中，亚马逊团队分享说，他们发现了一个复杂的错误，其最短的错误跟踪步骤为 35 步（!!）。该错误在广泛的设计审查、代码审查和测试中未被发现。亚马逊得出结论，如果他们坚持传统的测试方法，他们将无法发现它。
2. 那么，为什么不将所有事情都使用形式验证呢？
因为现实世界中的规范编写起来是一场噩梦。即使是像“在目录中查找行数最多的文件”这样的简单问题，在使用形式方法建模时也会变得复杂。我们必须回答诸如：“我们查看 ASCII 还是 UTF-8 换行符？不可读文件呢？符号链接呢？”等问题。没有形式方法，我们可以编写一个简单的验证，在 99%+ 的情况下是正确的。形式方法需要花费大量额外精力来处理不到 1% 的异常用例！
00:00 介绍
04:32 Crossover 项目
11:37 软件工程做得更好的地方
15:30 传统工程做得更好的地方
18:17 形式方法
29:32 TLA+：它是什么及演示
36:58 亚马逊的 TLA+
38:10 分布式系统失效的方式
41:03 形式方法与系统思维
46:20 学习数学的价值
50:23 TLA+ 的适用与不适用
52:50 Alloy：一种用于软件建模的声明式语言
58:53 其他形式方法工具
1:01:24 基于属性的测试
1:05:31 人工智能与形式验证的需求
1:12:29 程序员的逻辑
1:14:35 Hillel 对 2025 年人工智能影响的预测
1:21:30 书籍推荐
由以下机构提供：
• @AntithesisHQ – 无需人工审查或传统集成测试即可验证系统正确性，避免错误或中断。 https://t.co/AKYm4cctss
• @turbopuffer – 基于对象存储的向量和全文搜索引擎。快速、廉价且极具可扩展性。 https://t.co/w9y67GsFZJ
• @WorkOS – 让你的应用企业级就绪所需的一切。 https://t.co/aiAee0pcUP
与 Hillel 交谈时，我发现两件特别有趣的事情：
1. 亚马逊使用 TLA+ 发现了一个几乎无法通过形式方法找出的错误。
在论文《亚马逊如何使用形式方法》中，亚马逊团队分享说，他们发现了一个复杂的错误，其最短的错误跟踪步骤为 35 步（!!）。该错误在广泛的设计审查、代码审查和测试中未被发现。亚马逊得出结论，如果他们坚持传统的测试方法，他们将无法发现它。
2. 那么，为什么不将所有事情都使用形式验证呢？
因为现实世界中的规范编写起来是一场噩梦。即使是像“在目录中查找行数最多的文件”这样的简单问题，在使用形式方法建模时也会变得复杂。我们必须回答诸如：“我们查看 ASCII 还是 UTF-8 换行符？不可读文件呢？符号链接呢？”等问题。没有形式方法，我们可以编写一个简单的验证，在 99%+ 的情况下是正确的。形式方法需要花费大量额外精力来处理不到 1% 的异常用例！