Anthropic 在其官方研究页面发布了一项以“LLMs are making formal software verification feasible at a much larger scale”为主题的研究内容，归类为论文。该研究讨论大语言模型在形式化软件验证中的作用，目前公开信息为研究页面与这一核心判断，具体方法、实验设置与评测数据需以原文为准。
形式化验证指用数学手段证明程序满足其规格说明，而非仅靠测试抽样。长期以来，它的主要瓶颈不在理论，而在工程成本：需要专家把自然语言需求翻译成形式化规格，再在交互式定理证明器中逐条构造证明，工作量随代码规模迅速膨胀。因此，它多用于编译器、内核、密码实现等对正确性要求极高的少量场景，难以在普通业务代码中普及。
如果 LLM 能承担其中大量重复性、模式化的工作，例如协助撰写规格、补全引理、搜索证明策略、在证明失败时给出修改方向，形式化验证的适用边界就可能显著外移。对 AI 从业者而言，这一方向值得关注的原因在于它与常见的“模型生成代码”不同：证明是否成立由证明器机械检查，正确性不依赖对模型的信任，模型出错会被直接拒绝。这使得 LLM 的能力可以进入对可靠性要求最严格的那部分软件工程流程。
后续值得观察的是：这一路线在真实规模代码库上的可行性、对人类专家依赖程度的实际下降幅度，以及它与测试、静态分析等现有手段的分工。