LLM powered framework builds machine-checked proofs for C code safety
Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
Programming LanguagesSoftware Engineering
Summary
Verifying that complex C programs meet their requirements is hard because it needs detailed specifications and proofs that all parts work together correctly. The authors present a system called CCV that uses large language models to help build formal, checkable arguments that a C codebase is safe and meets its goals. CCV automatically creates specifications for functions and interfaces, checks proofs, and refines them iteratively with some human input. It has been tested on multiple real C projects, including cryptography code, with minimal human effort.
What this means in practice
- •For software verification engineers: Build machine-checked safety and correctness cases for C libraries automatically with limited human review.
- •For security software developers: Verify memory safety and correct interface usage in cryptographic C components to meet stringent security requirements.
Authors
Haokun Li, Zhongyi Wang, Guanyan Li, Xiao Yi, Shengchao Qin, Jianwei Yin, Mingshuai Chen
Abstract
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.