AutoRocq v1：程序验证证明义务

原作者将Frama-C程序验证义务送Rocq证明代理，并给Linux模块案例。

原文位置：§4、§5、§6.1、§7；代码24b92683d049aaa9ecf0cd19e247535e762f43b9

不能据此推出：641条SV-COMP引理分母不是641程序/完整内核；论文Rocq8.18，当前仓库9.0.0，不能静默继承成绩。

核查 2026-10-20 · 所属资料版本 2026-10-21.workunits.2 · 来源ID WU-M-AUTOROCQ

实际引用在哪里

程序验证专属生成证明与实际检查证据。

关系：直接对应

区分程序提取假设、引理与完整实现保证。

关系：相邻工作参照