代码可以足够精确地指定系统来正式验证它吗？

形式验证很少应用于生产软件，因为编写和维护模型的成本历来高于其回报。一项配套研究 [1] 使用成本较低的替代方案扩展了 SysMoBench [4]：根据从运行系统捕获的跟踪对规范进行分级。研究发现，当 大语言模型 编写规范时，可靠性由规范合约的结构决定，而不是由语言决定。本文对生产软件进行了评估：运营餐厅销售点系统的支付工作流程，该系统必须使收银机、支付终端和支付处理器保持一致。我们报告三个结果。首先，在精确陈述的故障模型下，核心协议相对于手工构建的、行引用的模型是正确的。审计发现了七个故障处理缺陷，几乎所有缺陷都有一个共同的根本原因；其中三个被复制为真实执行，并且在启用所有故障门的情况下重新检查关闭它们的补丁，之后后续补丁关闭了重新检查本身暴露的缺陷。故障模型的系统扩展（崩溃重新启动、陈旧读取、两次尝试）每个都找到了它们旨在探测的窗口。其次，对生产支付沙箱的一次探测暴露了响应形状差异，这使得整个恢复阶梯无法针对实时 API 进行访问。基于模拟器的审计无法检测到它，因为代码和模拟器有相同的误读：相关预言机故障。第三，配套研究的中心发现在两个供应商的七个模型中得到了重复：合同结构，而不是语言，可靠地控制着 LLM 指定的内容。复制涉及合约的排序和失败分类，而不是绝对水平：只有最强大的模型才能达到语料库上限，而更困难的任务会恢复基准测试失去的区分能力。