用 TLA+ 引导 AI 写代码：Mulga 以 AWS EBS 规范为例的探索

Mulga 正在探索用 TLA+ 形式化方法引导 LLM 写代码，并以一份真实的 AWS EBS 规范作为示例。TLA+ 由 Leslie Lamport 创建，基于形式数学记号，可对任何能表示为状态机的事物建立精确模型，并配套 TLC 穷举探索模型中的逻辑路径以发现设计问题。文章认为 TLA+ 不是代码而是数学，比编程语言更具表达力。