CCV：基于 LLM 从 C 代码自动构建机器可检的保证案例

CCV 是一个 LLM 辅助框架，用于从 C 代码库自动构建机器可检的保证案例，协调需求引导分析与自底向上规格构造，以及模块化证明与反馈修订两阶段。基于 VST in Rocq 实现，对 6 个 C 基准中全部 299 个函数定义验证了内存安全与无泄漏，每基准报告人工投入不足 1 人天。保证依赖披露的契约与假设，人工审查负责形式化制品与需求的一致性判断。