tla+

一档邀请 Hillel Wayne 的播客节目讨论了 AI 是否会推动形式化验证的主流采用，重点介绍了 TLA+ 在亚马逊的使用以及编写形式化规范的挑战。

介绍如何结合TLA+与Claude等LLM编写形式化规约，展示LLM如何在语法上提供帮助，同时专注于正确性。