标签
微软研究院及其合作者通过人类主导的智能体研究流程，解决了存在31年之久的KLS猜想，确立了对数凹分布的普适几何原理，并经独立研究者验证与机器形式化检验确认，为高维采样与随机算法效率理解扫清重大理论障碍。
普渡大学的一篇论文提出了一种有界的在线步骤级修复模块，用于 Lean 4 定理证明器。该模块将编译器错误信息输入预训练的修复模型，而不是直接丢弃失败的策略，在 LeanDojo 基准测试上求解率相对提升最高达 32%，并在 Lean Workbook 上性能几乎翻倍。
Maxwell 是一种新模型，能在运行时动态重写 Whisper 和 LTX-2 等 AI 程序的二进制文件以加速其运行，并使用形式化验证来确认优化后的版本保持了正确性。
doubleAI 发布 Maxwell，首个“代码执行模型”，可在程序运行时重写二进制以适配特定硬件与数据，并通过形式化证明保证优化等价，带来 38× 数据管线加速与 4.25× AI 推理内核加速。
Programming Language Foundations in Agda (PLFA) 是一本使用证明助手 Agda 讲解编程语言理论的开源教材，涵盖逻辑基础、操作语义与指称语义，并列出了多门采用该书授课的高校课程。
中国研究团队借助上海AI实验室自研的Intern-S2科学大模型，完整证明了困扰国际数学界30余年的三维Ghys猜想，随后由北京大学团队完成形式化机器验证，验证代码已全部开源。
Basis 研究人员利用 LLM 为一门小型编程语言编写形式化语义，并使用 Lean 证明编译到 RISC-V 后解释器符合这些规则。他们将现有解释器作为基准真值，以克服验证式软件中的规范瓶颈。
介绍 SentryWard：一个开源的 GPU kernel 形式化验证工具，可证明同步安全、无数据竞争与资源生命周期正确性，并通过系统性移除冗余同步使 NVIDIA B200 上的 kernel 最快提速 1.4 倍。
Lean v4.35.0 现已内置多个经验证的内核，包括 con-leche（首个拥有形式化一致性证明、由 Claude 实现的 Lean 编写内核）及其 Rust 优化版本 con-ron，以及新增的 `lake check` 命令，用于在外部重新检查开发成果。此举源于 AI 发现的内核健全性漏洞，旨在消除实现层面的不健全性，同时不带来性能损失。
介绍 IneqAgent，一个将大语言模型推理与符号计算结合的智能体框架，用于 Lean 4 中的不等式形式化证明，采用引理级蒙特卡洛树搜索协调引理构造与符号后端选择，在四个基准上达到 94.09% 的成功率。
该论文研究 Verus/Rust 形式验证工作流中，正确性反馈如何反而抑制规格完整性审计所需的证据，发现独立无反馈探索比带纠正反馈的循环产生多一倍的认证反例，并在 NeurIPS 2026 AI for Verifiable Coding 工作坊被接收。
QuixiAI 开源了 Sovereign Protocol Language (SPL)，一个基于 Lean 4 的形式化库，为"主权代理协议"(Protocol of Sovereign Agency) 提供规范性语义，核心包括 Duty、Power、Immunity 等原语以及 Law 3 非干扰实验，全部定理经内核验证、无公理依赖。
Materialize 介绍了它如何重构 `persist` 元数据存储，使用 PostgreSQL 的 READ COMMITTED 隔离级别而非 SERIALIZABLE 来构建可线性化日志，在一次亚稳态延迟事件后将写入吞吐量提升了三倍，并通过在 Lean 4 中对 PostgreSQL 的行为建模来证明可线性化，验证了正确性。
一个 GitHub 仓库展示了经机器验证的 Coq 证明，确定了新的忙碌海狸（Busy Beaver）冠军，其中包括一台 10 状态机，其得分超过了格雷厄姆数（Graham's Number）（快速增长层级中的 f_{ω+1} 级别），以无公理方式验证的精确得分击败了此前的 BB(8)、BB(9) 和 BB(10) 冠军。
Creusot 0.14.0 发布，这是 Rust 的形式化验证工具，新增了对偏序（partial orders）的支持以及为快照（snapshots）生成验证条件（VCs）的功能。
LeanPRM提出利用Lean证明助手自动为自然语言数学证明生成步骤级正确性标签，无需人工标注即可训练过程奖励模型（PRM）。Qwen3-4B验证器在该数据上训练后，步骤级标签准确率从48.2提升至74.7，并在IMO级问题的N选优选择和多个外部验证基准上超越使用PRM800K训练的验证器。
VEPA 是一个用于对 LLM 智能体的形式化护栏进行可验证演化的框架，采用由 LLM 提出的符号化策略补丁，并通过确定性验证器和具备证据感知能力的权限层进行验证，在智能体安全性与信息安全基准测试中优于基线方法。
LWN 报道了 Eurydice 项目——一个将 Rust 代码编译为结构清晰、可读的 C 代码的编译器工具，面向高可靠性软件验证场景，已用于后量子密码学例程的编译，由 Inria 与 Microsoft 团队维护的 Aeneas 项目的一部分。
OpenAI 利用其 AI 系统协助生成了与纳维-斯托克斯方程相关的形式化证明，但在形式化过程中，模型将部分数学内容错误地翻译成了代码。
一篇实操性很强的博客文章，通过在 Lean、Isabelle/HOL、HOL4 和 Agda 中分别形式化欧几里得证明素数无穷性的论证，对这四个定理证明器进行了比较，并给出了关于易用性、交互性和使用体验的带有个人主见的排名。