编码代理已经能够根据规格实现功能、编写并运行测试、修复错误并声明可发布。当同一代理系统同时生成软件和正确性证据时，测试套件不再是独立的依据：可见测试会被当作优化目标，代码与测试可能共享对规格的误解，构建者自己的测试也可能不完整。本文认为，代理生成的软件需要一个结构上独立于构建平面的保证层。我们将利益相关者意图与产出之间的差距划分为需求、符合、评估和模型四类，并分析验证能够弥合的部分。提出的框架将构建与验证分离，使用“验证合约”明确在发布前必须展示的内容，并将验证组织为两个阶段：第一阶段在不接触实现的前提下基于规格进行；第二阶段在获取实现后采用变异分析、属性测试和模糊测试。最终生成的保证报告交由人工决定是否发布。我们在预注册实验中对三种有状态服务（其中两种由第三方模型编写）以及一次 EvalPlus 试点进行评估。结果显示，构建者的程序本身是正确的，但其测试遗漏了细微交互：在全新上下文中的验证器检测到的 46 人为注入缺陷比构建者的测试多，Holm 校正后 p=0.006，同时揭示了规格的歧义，代价是极少数的错误判定。来自其他供应商的验证器未能提升检测能力。
点评