罗盘 / AI生成代码的形式化正确性证明
暗星档案 · 未点亮的星AI生成代码的形式化正确性证明
本条为初评草案（AI 辅助编目）：T 阶为三问初评（撬动面 × 停滞度 × 临界性），双评过 σ 门并红蓝复核后才升"已建档"。查不到的字段留空不编。点亮者会进入亮星候选流程，其贡献与星阶按 HCF 独立重评，不从暗星自动继承。
AI生成代码的形式化正确性证明T5 量级 · 新星
让AI写的代码自带可机器验证的正确性证明
暗星编号DS-0755
轴A · 可及性与成员福祉
领域ai-computing
状态初评草案 · 待双评与红蓝复核
这是什么 · 为什么难
AI 生成代码越来越多进入生产系统，但生成代码的正确性目前只靠测试用例和人工审查，无法穷尽边界情况。攻破意味着：AI 在生成代码的同时自动生成形式化规约（前置/后置条件）并用 Dafny、Lean 4 等验证器给出机器可检查的正确性证明，使高风险软件（金融清算、医疗设备控制、自动驾驶）中的 AI 生成代码具备可审计的数学保证，而不是「测试通过就上线」。
卡在哪 · 机制级卡点
在 FVAPPS 原论文的特定实验设置中，100 个程序样本共拆出 406 个定理；claude-3-5-sonnet-20241022 通过 121/406（约 30%），gemini-1.5-pro 通过 74/406（约 18.5%）。这组比例是特定模型版本、基准与脚手架下的定理通过率，不是大模型普遍的代码正确率。更深卡点仍是规约本身的自动生成：模型可能生成『能通过验证器但并非用户真正意图』的规约。
谁在攻
微软研究院（Dafny 相关工作）；VeriBench/FVAPPS 等基准的学术团队，具体机构未逐一核实
怎么参与
在 Dafny 或 Lean 4 上跑通一个简单函数的形式化验证教程，尝试让大模型补全验证注解并观察失败模式