代码能否精确指定系统以进行形式化验证？
Can Code Specify a System Precisely Enough to Formally Verify It?
AI总结：
研究评估生产软件支付工作流，通过手工模型验证核心协议正确性，发现故障处理差距并修复；生产支付沙盒探针暴露问题；还复制了关于大语言模型规范可靠性受合同结构而非语言影响的结论。
摘要：
形式化验证很少应用于生产软件，因其成本高回报低。一项研究用低成本替代方案扩展了SysMoBench。本文评估生产软件中一家餐厅销售点系统的支付工作流，报告了三个结果：核心协议在特定故障模型下正确；生产支付沙盒探针暴露问题；大语言模型规范可靠性受合同结构而非语言影响的结论可复制。
英文摘要：
Formal verification is seldom applied to production software, because writing and maintaining a model has historically cost more than it returns. A companion study [1] extended SysMoBench [4] with a lower-cost alternative: specifications are graded against traces captured from the running system. It found that when large language models write the specifications, reliability is governed by the structure of the specification contract, not the language. This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system, which must keep the register, payment terminal, and payment processor in agreement. We report three results. First, the core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model. The audit found seven failure-handling gaps, nearly all with a common root cause; three were reproduced as real executions, and a patch closing them was re-checked with all failure gates enabled, after which a follow-up patch closed a defect the re-check itself exposed. Systematic extensions of the failure model (crash-restart, stale reads, two attempts) each found the windows they were designed to probe. Second, a single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable against the live API. The emulator-based audit could not detect it, because code and emulator share the same misreading: a correlated-oracle failure. Third, the companion study's central finding replicates across seven models from two vendors: contract structure, not language, governs what LLMs specify reliably. The replication concerns the ordering of contracts and the failure taxonomy, not the absolute level: only the strongest models reached the corpus ceiling, and the harder task restores discriminating power the benchmark had lost.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
