Pre-QED 提出验证 Harness：把形式化验证的瓶颈从怎么证明转向证明什么
Pre-QED: Environment Specifications for Agentic Verification
搞形式化验证或 agent 做代码证明的人该看看。它点破了 OSS-Verify 这类方案只证明单条 fuzz 序列的局限，改用 LTL 建模 API 全部合法用法，还开源了挑战集，可以直接拿来测自己的证明 agent。
论文指出 LLM agent 让形式化验证规模化变得可行，但瓶颈已从"如何证明"转移到"证明什么"。以 Anthropic 与 Theorem 的 OSS-Verify 为例，它复用开源库的 fuzz harness 作为规格，让 agent 证明 harness 不会崩溃，但 fuzz harness 只覆盖单一调用上下文下的一条 API 调用序列，证明结果只对应一个使用场景而非整个库。
Pre-QED 提出"verification harness"：一种可执行的 harness，建模某个 API 的所有合法用法，使得对 harness 的证明等价于对每个行为良好的客户端的证明。构建流程采用 agentic 工作流，从代码与文档中提取 API 的使用契约，并用线性时序逻辑（LTL）排除非法的调用顺序。
作者同时指出证明 verification harness 面临的具体挑战，并将 harness 开源发布为社区挑战集。目标是让验证开源库像 fuzzing 一样成为常规操作，且保证覆盖所有合法客户端而非单一场景。
Pre-QED: Environment Specifications for Agentic Verification
LLM agents are making formal verification practical at scale. Recently, many attempts have raised this as an enticing possibility. However, formal verification at scale is only meaningful if deep formal specifications capturing functionality are available for checking. Unfortunately, recent works seek to bypass this issue by using shallow specifications devised for purposes other than verification. OSS-Verify from Anthropic and Theorem, for example, reuses the fuzz harnesses of open-source libraries as specifications and has an agent prove that each harness never crashes. However, a fuzz harness follows a single sequence of API calls under a single calling context, so the resulting proof covers one usage scenario rather than the library. We argue that the bottleneck of agentic verification has shifted from how to prove to what to prove. Before zooming into verification at scale, we need deep environment specifications to prove, which is why we call our effort Pre-QED. We propose verification harnesses, executable harnesses that model all legal usages of an API, so that a proof about the harness is a proof about every well-behaved client. To construct them, we use an agentic workflow that extracts the API's usage contract from code / documentation, and uses Linear-time Temporal Logic (LTL) to rule out illegal call orders. We identify the challenges in proving verification harnesses and release our harnesses open-source as challenges for the community. The overarching vision is that verifying an open-source library should become as routine as fuzzing it, with a guarantee that covers every well-behaved client rather than a single scenario like a fuzzing harness.
本条情报归属 AITOP「论文」核心栏目，重点聚焦北美前沿实验室与硅谷科技巨头。在跨区域产业观察坐标中，该动态直接关联「AI 开发者工具链、Coding Agent 与工程化实践」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：形式化验证、LLM Agent、LTL、OSS-Verify，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始信息发布自一手权威信源「arXiv: Anthropic」（Tier-1 一手发布），具备高确定性参考价值。截至目前，全网已有 11 家独立信源对该事件进行交叉印证与跟进报道（含 宝玉、AIGCLINK、berryxia 等），属于近期高关注度行业信号。
