面向智能体化证明 harness 工程的研究

论文提出一种智能体化证明 harness 工程师，可从软件项目和指定验证目标自动构建可供验证器使用的 harness，并结合形式化可靠性与精度守卫校验生成的抽象。作者在 curl 和 libuv 上做探索性案例研究，以源码中已存在的三处历史断言违规作为验证属性，结果显示该智能体构建的 harness 能让 CBMC 检出全部三处违规，并展示了这些 harness 在其他验证工具中复用的潜力。