一句话定义：AI 辅助形式化验证（AI-Assisted Formal Verification）指用大语言模型（Large Language Model, LLM）来写“待证明的数学命题”和“证明草稿”，再交给证明助手（Proof Assistant，如 Lean、Coq、Isabelle）逐步机器检查，从而证明一段协议或代码确实满足某项性质。
为什么以前难，现在变了
形式化验证的本质，是把“这段代码不会出某类错”翻译成一道数学证明题。比如对加密协议，你希望证明的不是“跑了一万次没出事”，而是“对任意输入序列，双方最终算出的密钥始终一致，且攻击者拿不到”。测试是抽样，证明是全称，差别就在这里。
难点在于写证明太贵：一个专家可能花几个月，只为几百行代码。LLM 恰好擅长其中的“翻译和补全”工作：把自然语言写的安全要求变成形式化规范（spec），猜出证明的主干结构，缺一个引理就补一个。打个比方，LLM 像一位反应快但会算错的学生，证明助手像不徇私情的阅卷老师。老师不关心答案是谁写的，只看每一步是否严格符合推理规则，错一步就报错。这个“LLM 提议、内核检查”的循环，是当前这类工作的主流形态。
DeepMind 与 Signal 合作，用 LLM 辅助把 Signal 协议的关键组件在证明助手中形式化，是这一方向的标志性案例：它说明真实工业级协议也能进入“可机检证明”的范围。具体进展与细节以官方发布为准。
和相邻概念的区别
| 手段 | 覆盖范围 | 能否给出保证 |
|---|---|---|
| 单元测试、模糊测试 | 有限样本 | 只能说明“这些情况没坏” |
| 静态分析 | 模式匹配、近似推断 | 会漏报误报，非全称 |
| AI 代码审查 | 依靠模型经验判断 | 输出是建议，不可机检 |
| AI 辅助形式化验证 | 对所有合法输入 | 证明通过检查即成立 |
关键区别在于：这不是“让 AI 看一眼代码说安不安全”，AI 的任何一步都必须过机器检查这一关，因此模型幻觉不会直接变成错误结论，只会变成“证不出来”。
对从业者的意义
对工程师来说，写规范仍然是人的活，而且是最难的一环：spec 写错，证明再漂亮也白证（garbage in, garbage out）。可机检的下游成本大幅下降后，小团队也有了做验证的可能。对普通人来说，意义在于你每天用的加密通信、芯片、数据库事务，其正确性依据可能从“我们测过了”慢慢变成“我们证过了”。这是一次把信任从“经验”迁移到“数学”的尝试，而 AI 正在把这件事的价格打下来。