**AI 代码验证的真相：形式化验证能证明什么？**

_AI proved your code correct. What did it actually prove?_

> 文章深入探讨了 AI 辅助编程中的形式化验证，指出 AI 生成的代码仅能证明其符合特定的数学规范（如排序函数的正确性），而非绝对真理。通过 Anthropic 和 GitHub 的最新研究，介绍了如何利用形式化验证确保代码无崩溃或满足安全策略，并强调了理解验证边界与规范假设的重要性。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-products
- **发布时间**：2026-11-11 09:01（北京时间）
- **原文**：[打开原文](https://kellerai.io/resources/ai-proved-your-code-correct)