主要观点：形式验证长期以来是发现分布式系统设计中细微错误的金标准，AI 已证明能加速验证过程，近期突破表明 AI 可从大型生产代码库中自动生成准确的形式规范，这标志着软件工程的一个关键转折点，预示着 AI 驱动的正确性验证将成为标准实践且可能优于人类努力。
关键信息：

• 以 GitHub Copilot 为例，其从 Azure Storage 生产源代码中自动生成精确的 TLA+规范，发现了传统代码审查和测试未发现的微妙竞态条件。
• AI 有 8 步方法，包括系统编目代码路径等、提取行为模式等、构建最小完整模型等。
• 从计划到执行过程中，AI 能自主分析代码、生成文档和规范，可迭代细化，通过模型检查发现问题并修正，还能通过 Git 历史分析发现遗漏的安全机制。
• 最终发现了旧主节点删除同时新主节点添加引用的关键竞态条件。
  重要细节：
• 开始让 Copilot 制定分析计划，Agent 按步骤执行，仅提供特征名和相关组件目录就可自主识别文件和提取信息。
• 发现初始规范缺失 etag 乐观并发控制机制后，AI 重新访问源代码并更新规范。
• 模型检查时先有语言错误被 AI 修正，后发现违反主安全不变量，AI 能定位问题序列。
• 通过 Git MCP 分析发现遗漏的悲观锁安全机制并更新规范。
• 展望未来，AI 可自主分析系统、发现不变量、自我验证规范、通过强化学习改进验证能力，最终在分布式系统正确性领域超越人类。