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

论文指出 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 一样成为常规操作，且保证覆盖所有合法客户端而非单一场景。