**AI生成的代码如何既可用又可证：形式化方法与AI的结合**

_AI-generated code that works – and proves it_

> Code Metal公司致力于构建AI驱动的代码翻译系统，特别针对安全与任务关键型软件（如航空航天、半导体、嵌入式系统等）。其核心挑战在于，不仅要生成可编译的代码，更要证明翻译后的系统能保持原始代码的行为与保证。文章指出，传统的软件测试无法穷尽所有可能输入，而形式化方法（一种数学严谨的技术）能够证明程序满足所有规格要求。该公司通过结合AI与形式化方法、差分测试、属性测试等软件保障技术，旨在解决高风险领域中代码转换的可信度问题，为关键基础设施提供更强的正确性保证。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-products
- **发布时间**：2026-05-19 06:00（北京时间）
- **原文**：[打开原文](https://www.codemetal.ai/research/ai-generated-code-that-works-and-proves-it)