# 程序与系统验证：规格、反例和证明产物相互对照

工作单元：W-M10；版本：2026-10-21.workunits.2；复核：2026-10-20
为指定实现交付可追溯的形式规格与验证结果，解释哪些实际要求已覆盖、哪些仍未证。

## 当前用法
固定规格/证明义务可整包委派生成与修复；从业务需求到系统规格先分阶段接收，按实际保证范围验收。
依据：AutoRocq在程序来源的641条SV-COMP证明义务中报告证明198条；分母是引理，不是完整程序。；DafnyBench评价模型给固定程序/规格补验证提示，并检查最终程序，而非自由修改规格求绿灯。
来源状态：active
本站记录：本站本任务AI运行数、成功率、实际成本及人工介入量均为null；代表例为交付设计，未执行。

条件：
- 需求与实现映射可审
- 验证工具和信任基础固定
- 独立缺陷/空洞证明控制

## 请求与范围
关键程序需验证、已有规格需维护，或模型检查给出反例需要定位真实缺陷。
需求到规格、环境抽象、代码/模型变更和验证同包；固定证明义务可以整包搜索，系统级规格需分阶段接收。不把Nexus数学成果当工业保证。

## 输入
- 真实需求与对象：固定代码/硬件模型、目标属性（安全性/活性/数值范围等）、接口/状态、外部环境假设、并发/内存模型和实现映射。
- 验证环境：指定Dafny/Rocq/Frama-C或模型检查器版本、solver/编译器、可信库/公理及允许改动区；超时/有限界说明。
- 独立控制：正例与能触发溢出/空集/并发等反例、已有测试/规格及旧版证明；不能只检查Agent写的assert。

## 交付物
- 需求—规格—实现/模型映射与假设/未编码需求清单
- 完整验证项目、锁定工具/solver、证明脚本/模型检查状态及原始日志
- 可重放反例及其映射：真实代码缺陷、规格错误或抽象伪反例
- 验证驱动代码/规格差异与回归、升级后的证明维护/信任基础记录

## 验收
1. 证明的属性对应真实需求
   方法：独立对照需求、前/后置条件、状态/环境假设；检查可满足性和vacuity，确认不是把期望写进前提。
   拒收：requires false导致全通过；数学整数模型掩盖机器溢出。
2. 形式结果实际完整
   方法：干净重建并检查admit/axiom/assume/disabled proof、solver/库依赖；有限模型/超时/unknown各自标识，不用“无反例”混成无界证明。
   拒收：跳过失败义务、增加未批准公理；仅有限展开却声称全局活性。
3. 反例与实现连接
   方法：重放trace及输入，核对环境可达性；真实缺陷变成独立回归，伪反例记录需要加强的抽象。
   拒收：反例只在不可能环境出现；为消除反例删真实需求。
4. 变更保持目标和信任边界
   方法：比较固定规格/代码diff，重新运行受影响证明/模型检查和实现测试；记录编译器/FFI/硬件连接的保证缺口。
   拒收：证明旧代码，部署新代码；依赖版本变而缓存仍绿。


## 具体例子
输入：设计例：固定32位数组求和函数，约定长度/元素范围和溢出行为；要证明结果与数学和一致并保持边界安全。
预期产物：代码—规格映射、溢出义务/不变量/证明或trace、锁定项目与变更回归；本例未运行。
失败：只在无限整数模型证明求和，却对32位实现声称无溢出；加入false前提通过。

## 工作重组
以前：需求专家写规格，开发改代码，验证者补证明，变化后返工。
现在：代理可提出规格/不变量、探索反例、修改代码并响应验证器；可信需求/规格边界独立检查，固定义务无需逐步批准。
保留：
- 真实属性与环境假设确认
- 保证用于部署的接收责任
新增：
- 空洞规格/未证义务检查
- 反例到代码的映射
- 证明与实现版本同源

## 人的责任与失败接管
需求/验证接收者确认期望属性及模型含义，代理可承担证明、反例和变更搜索；验证工具承担形式判断，部署负责人确认未建模条件。
unknown/timeout保留具体义务与预算，不作unsafe或safe结论；反例先辨真伪，不通过弱化规格消除；环境缺失交可重放最小项目。

## 尚待补足
- 并发/硬件/大型规格没有本包直接AI完成率
- 证明不覆盖未建模需求或完整可信编译链

## 职业与团队下一步
形式方法、程序验证、验证工程
规格/实现映射、证明/反例、信任基础及维护差异
补目标语言/系统语义，展示一次空洞证明如何被拒。
/explore?purpose=career&domain=math
规格建模还是证明细节/维护耗时？
代理做候选模型/证明与反例，领域接收者审属性和现实连接。
分开统计规格错误、义务失败和工具chain阻塞。
/explore?purpose=team&domain=math

## 证据与关系
- AutoRocq v1：程序验证证明义务：https://arxiv.org/html/2511.17330v1
  定位：§4、§5、§6.1、§7；代码24b92683d049aaa9ecf0cd19e247535e762f43b9；公开 2025-11-21；核查 2026-10-20；复查 2026-11-20
  支持：程序验证专属生成证明与实际检查证据。；区分程序提取假设、引理与完整实现保证。
  未覆盖：不等于198完整工业系统通过；未覆盖全部需求与编译/硬件链。；系统级规格、并发/硬件变体需新任务验证。
- DafnyBench v1：程序证明注解补全：https://arxiv.org/html/2406.08467v1
  定位：Benchmark construction / evaluation；官方sun-wendy/DafnyBench；公开 2024-06-12；核查 2026-10-20；复查 2026-11-20
  支持：固定规格下的程序验证注解任务证据。
  未覆盖：有限程序、历史模型；不保证自动写对需求或整个工业系统。


## 任务级判断与证据
采用方式：分阶段接收
从证据到建议：DafnyBench和AutoRocq提供程序专属证明证据，支持把细节搜索交给代理；它们并未证明任意生产系统规格正确，因此独立验收需求/模型连接而不只看证明通过。
当前可用性：mixed；公开资料和工具入口已核对；论文配置、当前实现声明及本任务成绩分别记录，未运行本任务。
- AutoRocq：https://github.com/NUS-Program-Verification/AutoRocq/tree/24b92683d049aaa9ecf0cd19e247535e762f43b9
  24b92683…；仓库Rocq9.0.0，论文8.18；开源Python/opam/Docker、模型API；不把新工具链继承旧成绩。
- DafnyBench：https://github.com/sun-wendy/DafnyBench
  论文v1；代码执行前锁commit及Dafny/solver版本；公开ground_truth/hints_removed/eval；未安装运行。

### AutoRocq在程序来源的641条SV-COMP证明义务中报告证明198条；分母是引理，不是完整程序。
依据身份：外部报告结果；状态：active
- AutoRocq v1：程序验证证明义务：https://arxiv.org/html/2511.17330v1
  定位：§5.1/§6.1/§7；关系：direct
  支持：程序验证专属生成证明与实际检查证据。
  限制：不等于198完整工业系统通过；未覆盖全部需求与编译/硬件链。
  核查：2026-10-20；来源状态：active
配置：arXiv v1；GPT4.1 temperature0；论文Rocq8.18/CoqPyt1.0.0、Frama-C WP提取；641义务含不溢出/功能/不变量，当前仓库9.0.0另记。
适用限制：不等于198完整工业系统通过；未覆盖全部需求与编译/硬件链。
相关进展（本条判断）：
- 程序验证代理交付可重放Rocq证明义务：/explore?purpose=understand&domain=math&window=all#P-M-PROGRAM-PROOFS
  首次公开 2025-11-21；判断变化 2025-11-21

### DafnyBench评价模型给固定程序/规格补验证提示，并检查最终程序，而非自由修改规格求绿灯。
依据身份：外部报告结果；状态：active
- DafnyBench v1：程序证明注解补全：https://arxiv.org/html/2406.08467v1
  定位：dataset construction / evaluation；关系：partial
  支持：固定规格下的程序验证注解任务证据。
  限制：有限程序、历史模型；不保证自动写对需求或整个工业系统。
  核查：2026-10-20；来源状态：active
配置：arXiv v1；750余现有Dafny程序移除提示，原模型/反馈条件以论文为准；本文不转抄分数。
适用限制：有限程序、历史模型；不保证自动写对需求或整个工业系统。
相关进展（本条判断）：
- 程序验证注解已有可重放任务评价：/explore?purpose=understand&domain=math&window=all#P-M-DAFNY
  首次公开 2024-06-12

### 接收必须包括需求/模型映射和完整义务，不能由局部证明通过推出现实系统安全。
依据身份：有条件的编辑推断；状态：active
- AutoRocq v1：程序验证证明义务：https://arxiv.org/html/2511.17330v1
  定位：§5生成义务；§7案例；limitations；关系：adjacent
  支持：区分程序提取假设、引理与完整实现保证。
  限制：系统级规格、并发/硬件变体需新任务验证。
  核查：2026-10-20；来源状态：active
适用限制：系统级规格、并发/硬件变体需新任务验证。

## 情境变化
### 固定局部证明义务
输入变化：规格与代码已可信，只缺证明/不变量。
判断变化：可整包委派直到完整核验；接收范围就是该义务。
验收变化：防改规格/加假设/漏依赖，不能扩成全程序完成。
### 并发或硬件系统模型
输入变化：时序、公平性、缓存/通信/硬件抽象影响性质。
判断变化：可交形式模型与反例候选，缺专属AI实测；分阶段接收模型。
验收变化：安全/活性、状态界与公平性/环境假设，trace到真实状态映射；软件算术证据不转移。
### 规格/代码升级
输入变化：依赖、接口和实现一起演进。
判断变化：可委派证明维护及影响分析，先锁定不允许弱化的属性。
验收变化：重放受影响义务和负控制，区分新旧版本覆盖。
### 顺序软件规格与验证
输入变化：固定顺序软件模块、机器整数/内存语义和目标属性，不以并发/硬件抽象为前提。
判断变化：可委派规格/证明/反例候选；需求对应先接收，已有可信规格下按完整义务接收。
验收变化：查需求—前后置/状态—代码对应、可达性/vacuity、完整义务与实现测试，边界/溢出及反例重放。

研究前沿：已公开从C验证义务到Rocq脚本及Dafny注解的代理路径；新仓库工具链与论文旧版本不同，需重放。
下一项验证：用固定小型C/Dafny模块，先用vacuous requires、溢出和错误不变量校准验收；隐藏参考证明，检验完整义务、代码映射和一个修改后的维护。
未来改判信号：
- 扩大：未见真实模块/变更中规格覆盖、反例映射与完整义务持续通过，维护成本可控。
- 收缩：只补局部引理而漏主目标、依赖大量assume或现实模型不符；缩到局部义务。

## 与本单元直接关联的进展
### 程序验证代理交付可重放Rocq证明义务
公开 2025-11-21；判断变化 2025-11-21
程序来源的证明义务有专属代理成果。
支持范围：局部引理和Linux模块案例不等于完整内核验证。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-PROGRAM-PROOFS

### 程序验证注解已有可重放任务评价
公开 2024-06-12
固定程序/规格下补全验证提示不同于数学解题。
支持范围：不证明业务规格正确或整个系统安全。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-DAFNY

领域背景与未来情景：/explore?purpose=understand&domain=math


## 工具与采用佐证