蓝图而非提示词：用 TLA+ 指导 AI 编写代码
Mulga 的一名工程师指出，随着 AI 编写了大部分生产代码，团队正在失去曾经沉淀在代码库中的共识，他提出用 TLA+ 形式化规范作为可机器校验的蓝图——由人类设计、AI 实现，并以仅约 400 行的 AWS EBS 卷生命周期开源 TLA+ 规范作示范，而 AWS 的相关文档足有 13 页且语义含糊。这个想法很重要，因为它重塑了 AI 时代的工程分工：精确的规范成为人类拥有的核心产物，实现则成为可替代的环节，交给代码智能体完成。
报道来源 · SOURCES
- Hacker News (AI)2026-10-21 03:03