formal-verification

PULSE is a new executable contract language for spatiotemporal knowledge graph engineering, providing a typed runtime with role-based write effects, safety properties verified in Lean 4, and trace parity across large datasets.

本文为工作流持久化层中的检查点、中断和恢复语义引入了一种机器检查的一致性契约，并对多个智能体工作流框架进行了实证评估，发现没有完全符合的框架。本文还提出了一个参考实现以及针对跨进程消费的修复。

OpenAI 发布了十项由 AI 在数学和理论计算机科学领域取得的进展的手稿、正式的 Lean 证书和推理演练，其中包括球体堆积、非 sofic 群和量子并行重复方面的结果。

This paper introduces an inprocessing framework for neural network verification driven by lookahead lemmas, improving the performance of verifiers Marabou and α-β-CROWN by proving up to 34% more instances unsatisfiable.

This paper proposes efficient search methods to locate verdict boundaries in Branch and Bound (BaB) neural network verification, leveraging path monotonicity to skip irrelevant subproblems and improve verification efficiency.

ModelEquivBench 是一个面向 LLM 生成优化模型的认证式多关系评估系统，报告逐对语义概况（涵盖七种等价关系），而非单一的准确率分数。它在固定基准上评估了 GPT-5.4、Claude Sonnet 4.6 和 Qwen3.5-397B-A17B，揭示了粗粒度基线无法发现的阶段式失败。

本文介绍了一种三阶段LLM流水线，用于系统性地生成和验证重大数学猜想，利用Lean 4形式化验证和反思性验证来发现具有高“问题品味”的问题。

F* 是一种通用的、面向证明的编程语言，它将依赖类型与基于 SMT 和策略驱动的证明自动化相结合，可编译为 OCaml 及其他目标语言。这是一个由微软研究院、Inria 和社区共同开发的开源项目，用于形式化验证。

对 Lean 内核中一个可靠性漏洞的事后剖析，该漏洞被利用来产生考拉兹猜想的“反证”，并说明了修复方案以及为什么独立的检查器最初也未能发现它。

Lawrence Paulson 讨论了因 Lean 内核中的一个 bug 导致的 Collatz 猜想的虚假反驳，并对证明对象和证明助手的可靠性进行了思考。

This paper introduces a property-driven causal abstraction technique for factored Markov Decision Processes (MDPs), grouping states based on causal relations over state variable predicates to reduce model size while preserving property-relevant behavior. The approach is evaluated on standard benchmarks, yielding small abstractions that support near-optimal policy computation and often generalize to larger MDPs.

一本实用的书，面向程序员介绍逻辑，以改进软件设计、验证和推理，涵盖从简化条件语句到形式化验证和约束求解等主题。

一档邀请 Hillel Wayne 的播客节目讨论了 AI 是否会推动形式化验证的主流采用，重点介绍了 TLA+ 在亚马逊的使用以及编写形式化规范的挑战。

一篇技术博文认为，由于Rocq（Coq）原生支持余归纳类型和cofixpoints，而Lean基于库的方法尚不成熟，因此Rocq在程序验证方面优于Lean。

本文介绍了为ARCH HDL（一种面向AI模型生成的硬件描述语言）设计并端到端形式化验证IEEE-754 binary32和bfloat16算术。这些算子通过结合穷举SMT等价性检查和Lean 4证明的混合方法，被证明具有正确的舍入，并输出可综合的SystemVerilog。

本文讨论了LLMs如何自动生成证明，在如Lean和Rocq这样的依赖类型语言中，通过利用证明无关性并减少手动证明工程的需求，使得形式验证变得更加实用。

一篇博客文章展示，经形式化验证的Lean实现的DEFLATE压缩算法在典型级别上，其速度和压缩比均优于纯Rust实现。作者将此归因于能够安全地让AI代理优化代码，并依赖形式化证明来保证正确性。

OCaml 创建者 Xavier Leroy 在访谈中讨论了 OCaml 的设计优势、与 Rust 和 JavaScript 的对比、类型推断原理以及函数式编程的学习难度。

一个经 Lean 验证的新形式定理表明，对于趋向无穷的阈值，几乎所有正整数都在 436 ln N 个 Collatz 步内降至该阈值以下，强化了陶哲轩先前的结果，并给出了显式界限和自然密度。

本综述为强化学习策略的验证方法提供了统一视角，提出了一个按三个维度（验证范式、时间范围和保证强度）分类的方法，并指出了新兴研究方向。