蓝图而非提示词：Mulga 探讨用 TLA+ 形式化方法指导 AI 编写代码

Mulga 工程师 Bryn 指出大模型代写代码正在削弱团队对系统逻辑的掌控，提出应使用 TLA+ 形式化规范作为系统蓝图来指导与检验 AI 编码。文章结合约 400 行开源 AWS EBS 状态机规范的实践说明，自然语言提示词歧义过多且难以穷举边缘情况，而 TLA+ 能够以严谨的数学状态机抽象关键意图，配合 TLC 模型检验为 AI 生成代码提供可机检的基准。