发表机构
Zhejiang University; University of Oxford; The Chinese University of Hong Kong; Xidian University（浙江大学; 牛津大学; 香港中文大学; 西安电子科技大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出CCV框架，利用LLM辅助构建机器检查的保证案例，通过接口协议和模块化证明验证C代码库满足需求，在六个基准上验证299个函数，人工工作量低。
AI 中文摘要
大型语言模型（LLMs）在自动化交互式定理证明方面显示出潜力，然而对现实世界C代码库的验证不仅仅需要解决单个证明目标。该任务涉及联合构建表达性函数规范及其证明，并确保库接口在无指定客户端的情况下沿预期调用序列组合。本文提出CCV，一个LLM辅助框架，用于构建机器检查的保证案例：支持C代码库满足其预期需求的结构化、可审计工件。为建模开放库中预期的跨接口使用，CCV构建一个接口协议，暴露允许的调用序列和资源假设以供审查，并在验证契约和调用方义务下提供条件性安全保证。CCV协调两个互补阶段：（i）需求引导分析和候选规范及协议的从下至上构建；（ii）带反馈的模块化证明构建，修订规范和证明。使用Rocq中的VST实现，CCV验证了六个C基准中所有299个函数定义的内存安全和泄漏自由，包括工业密码组件，每个基准报告的人工工作量不到一个人日。保证依赖于披露的契约和假设；人工审查提供连接形式工件与预期需求的一致性判断。
英文摘要
Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proof goals. The task involves jointly constructing expressive function specifications and their proofs, and ensuring that library interfaces compose along intended call sequences even without a designated client. This paper presents CCV, an LLM-assisted framework for building machine-checked assurance cases: structured, auditable artifacts supporting the claim that a C codebase meets its intended requirements. To model intended cross-interface use in open libraries, CCV constructs an interface protocol that exposes permitted call sequences and resource assumptions for review, with a conditional safety guarantee under verified contracts and caller obligations. CCV coordinates two complementary phases: (i) requirement-guided analysis and bottom-up construction of candidate specifications and protocols; and (ii) modular proof construction with feedback that revises the specifications and proofs. Implemented using VST in Rocq, CCV verifies memory safety and leak freedom for all 299 function definitions across six C benchmarks, including industrial cryptographic components, with less than one person-day of reported human effort per benchmark. The guarantees depend on disclosed contracts and assumptions; human review supplies the conformance judgments connecting the formal artifacts to the intended requirements.
