Pre-QED 提出验证 Harness：把形式化验证的瓶颈从怎么证明转向证明什么

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.

This report is categorized under AITOP's "Papers" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include 形式化验证, LLM Agent, LTL, OSS-Verify.

Primary source verification: published directly by arXiv: Anthropic with first-party authority. Cross-source corroboration: 11 independent sources have covered this development (including 宝玉, AIGCLINK, berryxia), confirming industry-wide signal strength.