我们现在有了证明自动化
长期以来被视为成本过高且过于专业的软件形式化验证，正因大型语言模型而发生变化：它们如今可以在 Lean 等系统中生成并自动化许多证明。评论者认为，这可能让高保证代码，甚至已验证汇编，在更多领域变得可行，尤其是在安全关键领域；但他们也强调，编写好的规范和抽象仍然是难点，而且如果规范有缺陷，形式化方法仍可能把“错误的行为”证明为正确。关于依赖类型和全函数在真实世界维护中的可扩展性，以及 LLM 驱动的验证是否会真正改变主流软件工程实践，还是只会集中在关键边界情况上，仍存在激烈争论。
LLMs + 证明自动化
- 许多人认为 LLMs + 定理证明器（Lean、HOL 风格系统等）带来了范式级变化：它们现在可以处理过去需要数天或数周才能完成的证明的大部分内容。
- 证明无关性加上自动化，或许会让富依赖类型系统变得更实用，从而减少“证明工程”工作量，不过良好的问题拆分和抽象仍然至关重要。
- 有些人描述了成功实验：LLMs 在几分钟内重现了原本需要数天的形式化证明，这暗示此前“疯狂”的验证项目（内核、重大定理）如今可能变成可由单人完成的工作。
规范是瓶颈
- 几位评论者认为，最难的不是证明正确性，而是定义什么才算正确：现实世界的软件往往没有针对边界情况的精确定义（网络故障、备份、序列化器等）。
- 编写形式化规范的篇幅和复杂度可能超过代码本身；规范中的 bug 会直接转化为“已验证但错误”的系统。
- 部分规范（例如往返一致性、压缩/解压互为逆、“绝不执行任意代码”）仍然被认为非常有价值。
依赖类型、维护与语言设计
- 一派观点认为，依赖类型和全函数在大型系统中无法扩展：添加一个新属性可能需要在许多类型和证明中传递新的不变式。
- 反方观点：这与任何大型系统中维护正确性是类似的；良好的结构化方式（职责分离、使用不透明类型、小型可信核心）可以缓解这种痛苦。
- 将验证集成到类型系统中的未来语言被视为很有前景，但许多人预计大多数程序只会验证关键部分，而不是整个系统。
安全、密码学与已验证汇编
- 区块链和密码学被视为首要候选场景：强对手、形式化方法的历史，以及对已验证汇编和编译器的兴趣。
- 随着利用漏洞的成本下降（包括通过 AI），有人认为形式化验证在经济上会变得更有吸引力；也有人认为组织会止步于“足够好”的自动化漏洞发现。
LLM 行为、对齐与局限
- LLMs 往往会避免高强度的证明工作，除非被强烈提示；它们偏好表面化的解决方案，并且可能在没有强制要求时忽略强大的库。
- 它们也可能错误地实现某个功能，然后生成测试/规范来“证明”错误行为，因此对规范进行人工审查仍然至关重要。
- 赞同者认为形式化方法 + LLMs 具有变革性；怀疑者则警告说，这主要只是把难点转移到了更高层级的规范上，并不会取代测试或人的判断。