pre-QED 用智能体生成验证桩，建模 API 合法用法

Greetings from Singapore. Announcing pre-QED, providing environment specifications prior to AI-based verification. Formal verification at scale using AI, is a topic of high interest today. However, when we are verifying a piece of code, we need to verify it under all possible environments, and not just one possible scenario. The recent work of @AnthropicAI and @theoremlabs re-uses fuzz harnesses for verifying absence of crashes. However, a fuzz harness follows a single sequence of API calls under a single calling context, so the resulting proof covers one scenario,  rather than verifying  the library. This is a core principle our team at NUS  is well aware of, after more than a decade of developing greybox fuzzing technology. 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. Most importantly, we automatically generate these verification harnesses using an agentic workflow, they do not need to be manually written. Use our verification harnesses in AI-based verification - so that we can achieve ACTUAL software verification at scale using AI.  See https://pre-qed.github.io Ack: NRF Singapore AI for Science research program.