AI写的代码，到底能不能"锁死"安全底线？

AI批量生成代码的浪潮里，一个老问题始终悬着：我们凭什么相信那些模型吐出来的逻辑没有隐藏地雷？MAGS这篇论文试图给出一个硬核回答——用形式化验证把安全属性"机器校验"，让机器证明机器写的代码靠谱。思路不算新，把HOL、Coq那套工具链往AI生成代码的场景上接，但关键在于它瞄准的是"指定安全属性"这个粒度：不是要证明整个程序正确，而是把开发者关心的关键不变量抽出来，跑一遍形式化推导。这比传统测试覆盖率检查高了一个维度。我的判断是，这条路不会替代代码审查，但在金融交易、自动驾驶这类"出错就是事故"的场景里，它是目前唯一能把信心从"大概率没问题"推到"数学保证没问题"的技术。问题是，谁来写这些形式化规约？如果写规约本身也靠AI，这循环就没闭合。

原文：MAGS: Machine-checked guarantees on specified safety properties in AI code · 来源：Hacker News