Source-linked AI summary
Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
Haokun Li, Zhongyi Wang, Guanyan Li, Xiao Yi, Shengchao Qin, Jianwei Yin, Mingshuai Chen
TL;DR
Real-world C verification requires more than proving individual functions: specifications must jointly support intended requirements, including interface call sequences in open libraries. CCV builds machine-checked assurance cases through coordinated specification and proof construction, using an interface protocol to model cross-interface use. It verifies memory safety and leak freedom for 299 function definitions across six benchmarks, while disclosed assumptions and human conformance review bound the claims.
Problem
Proof-construction automation does not establish that function specifications collectively conform to intended requirements, including the call sequences expected of open libraries.
Source: §1 · p. 2, §2.2 · p. 4Method
Results
CCV establishes 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.
Source: §1 · p. 2, §8 · p. 17Takeaways & Limitations
The assurance cases combine machine-checked evidence with human conformance review connecting formal artifacts to intended requirements.
Source: §8 · p. 17The protocol’s safety guarantee applies under verified contracts and stated caller obligations, and does not verify arbitrary clients.
Source: §4.3 · p. 10
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Automating individual proofs does not by itself establish that a real-world C codebase meets its requirements: specifications must be jointly proved and shown to compose as intended. CCV builds machine-checked assurance cases using a two-phase workflow and an interface protocol, and evaluates it across six C libraries.
Motivation
- Proof automation alone leaves open whether a codebase’s specifications collectively conform to its intended requirements, beyond whether implementations satisfy them.The paper frames this as the need for an auditable end-to-end assurance case.Source: §1 · p. 2
- Function specifications and proofs must co-evolve because proof attempts reveal when a contract is too strong, too weak, or mis-expressed.Prior approaches that prove stated theorems take specifications as given, while contract synthesis approaches described here stop short of machine-checked body proofs.Source: §1 · p. 2
- Open libraries need library-level conformance evidence because separate module proofs do not establish that interfaces support the required call sequences.CCV’s interface protocol makes permitted calls and resource assumptions reviewable, with a conditional safety guarantee under verified contracts and caller obligations.Source: §1 · p. 2
Approach
- CCV coordinates requirement-guided specification and protocol construction with modular proofs, using proof feedback to revise specifications, protocols, and proofs.The two phases connect function-level verification to library-level requirements expressed through the protocol.Source: §1 · p. 2
Evaluation
- CCV verifies memory safety and leak freedom for all 299 function definitions across six C libraries, with less than one person-day of reported human effort per benchmark.The evaluation includes four cryptographic components of openHiTLS; human review supplies the conformance judgments linking formal artifacts to intended requirements.Source: §1 · pp. 2–3
2 BACKGROUND AND MOTIVATION
The motivating examples show that function contracts and proofs constrain one another, while individually verified interfaces may still fail to compose along intended call sequences. The section frames these as distinct function-level and library-level verification challenges.
2.1 Function-Level Verification
- Function-level verification jointly constructs a function’s specification and a machine-checked proof that its body satisfies that specification.The paper’s example presents the proof as a Hoare-style judgment against a VST/Rocq specification.Source: §2.1 · p. 3
- The initial list_length contract cannot prove the loop’s increment safe; adding the precondition Zlength xs <= Int.max_signed closes the signed-overflow obligation.The example illustrates how a proof can require a stronger specification, which in turn enables the body proof.Source: §2.1 · p. 3, Figure 1 · p. 4
2.2 Library-Level Conformance
- Library-level conformance concerns whether exported interfaces, taken together, support intended requirements over legal call sequences.Function proofs alone do not establish this cross-interface property, and existing LLM-assisted methods described here focus on function-level verification.Source: §2.2 · pp. 4–5
- Individually verified interfaces may not compose: weak list_push and list_remove postconditions do not preserve the length information needed to call list_length.Revised postconditions retain the list transformations needed to establish the next call’s precondition; both versions are provable, but only the stronger revisions conform to requirements.Source: §2.2 · p. 5, Figure 2 · p. 5
3 THE ASSURANCE CASE
CCV’s assurance case combines machine-checked formal artifacts with a human review connecting those artifacts to design requirements. For open libraries, it uses an interface protocol; libraries with an in-scope client instead use client-level evidence.
3 THE ASSURANCE CASE
- CCV generates function specifications and proofs, and for open libraries constructs a protocol and proves accepted interface-call sequences safe under the verified specifications.The codebase is translated to a Clight AST; the remaining manual obligation is reviewing whether specifications and protocol conform to the requirements.Source: §3 · p. 6
- Human review judges whether the function specifications and interface protocol conform to the requirements, including whether preconditions are too strong or legal safe sequences are omitted.Source: §3 · p. 6
- When a library contains an in-scope client, CCV replaces the interface protocol with a client-level specification and whole-program evidence.Source: §3 · p. 6
4 THE INTERFACE PROTOCOL FOR OPEN LIBRARIES
CCV models intended use of an open library as a state-based protocol because no designated client delimits the permitted interface-call sequences. Its states, guards, and call branches make those sequences and their assumptions explicit, guiding interface synthesis and refinement.
4 THE INTERFACE PROTOCOL FOR OPEN LIBRARIES
- The interface protocol makes requirement-permitted call sequences and their assumptions explicit for expert review, while guiding synthesis and reconciliation of interfaces that do not compose.The need arises because an open library has no client control flow to delimit legal sequences.Source: §4 · p. 6
4.1 Protocol States and Behaviors
- Each function interface maps caller-instantiated logical variables to concrete C arguments and gives preconditions and postconditions over pure propositions and spatial resources.Observable post-call values include return values or values written through out-parameters.Source: §4.1 · p. 7
- For list_length, the protocol example instantiates logical inputs with a list pointer and abstract list, and its postcondition's pure component includes the decoded return constraint.The mathematical integer represented by the concrete C return value is used as the return value.Source: §4.1 · p. 7
- Protocol states track library globals, borrowed client resources, and library-managed objects; their interpretation includes an invariant that must hold before and be re-established after each call.Source: §4.1 · p. 7
- A protocol branch records the next state, observable results, a pure result fact, and residual resources not represented by that state.Source: §4.1 · p. 7
The last two components in (2) are the per-function families
CCV’s per-function guards and branches describe permitted calls and possible outcomes, while protocol edges connect those abstract transitions to resource-aware function interfaces. Protocol soundness is conditional on verified contracts and caller obligations, and review and disclosure address limits that the theorem does not resolve.
The last two components in (2) are the per-function families
- Per-function guards determine whether a call is permitted at a state and input, while branches describe its possible successor states and outcomes.In the linked-list example, the length guard requires the target list to be recorded in the state and its length to fit the integer bound.Source: The last two components in (2) are the… · p. 8
4.2 Protocol Edges and Subsumption
- A protocol edge summarizes all branches for a source-state/function pair, connecting the interface’s resource-independent contract to state-specific resource flow.Per-edge subsumption ensures permitted calls meet the interface precondition and interface outcomes fit declared branches, but extra declared branches may never occur.Source: §4.2 · pp. 8–9
4.3 Input-Aware Runs and Protocol Soundness
- Under H1 and H2, every concrete execution realizing a valid input-aware run is safe, and returned edge postconditions supply successor states for subsequent calls.The safety argument covers finite runs and finite prefixes of infinite runs; the client must meet the recorded argument and ownership obligations.Source: §4.3 · p. 10
4.4 Model Quality, Review, and Limits
- Protocol scrutiny requires a satisfiable covering witness, model-fidelity checks, and human review; soundness does not establish completeness with respect to requirements.The model lacks a client-side checker and does not prove termination, branch liveness, or callback and concurrent ownership protocols.Source: §4.4 · pp. 10–11
5 CCV FRAMEWORK: AN EVIDENCE-PRODUCING WORKFLOW WITH REVIEW GATES
CCV organizes assurance construction as an evidence-producing workflow with agent-built artifacts and human review gates. Its stages establish the program and contractual demands, formalize specifications and protocols, then prove and audit them within disclosed trust boundaries.
5 CCV FRAMEWORK: AN EVIDENCE-PRODUCING WORKFLOW WITH REVIEW GATES
- CCV’s workflow combines agent-produced assurance artifacts with human review of scope, assumptions, and design conformance; a successful run records both machine-checkable evidence and human judgments.All agent-working states apply to open libraries and libraries with a designated main; V_Specify produces a protocol configuration for the former and a main-level specification for the latter.Source: §5 · p. 11
- V_Review is an optional early gate, but successful runs pass through V_Confirm, which can request tracked rework when artifacts do not reflect reviewer decisions.Early review can send the run back to preprocessing; V_Confirm assesses the proof and protocol artifacts, and successful delivery does not claim universal program correctness.Source: §5 · p. 12, Figure 5 · p. 12
5.1 V_Preprocess: Establishing the Frozen Clight Program
- V_Preprocess establishes a reproducible frozen Clight program and records input provenance, transformations, and scope.For adaptations that change the program or replace environment behavior with new assumptions, CCV claims no preservation of the original C semantics and submits the change for review.Source: §5.1 · p. 12
5.2 V_Analyze: From Code and Design Material to Contractual Demands
- V_Analyze derives candidate contracts, assumptions, invariants, and open-library usage constraints from callers, implementations, and design material.Its analysis record documents a basis for formalization, not a soundness theorem; it also records assumptions and analysis-to-specification choices for later review.Source: §5.2 · pp. 12–13
5.3 V_Specify: Formalizing Specifications and the Protocol Configuration
- V_Specify formalizes resource predicates, lemmas, function specifications, and— for open libraries—protocol states, transitions, and edge specifications.It proceeds from callees to callers and records natural-language-to-formal changes; compilation does not establish design conformance, which remains for human review.Source: §5.3 · p. 13
5.4 V_Prove: Discharging and Auditing Proof Obligations
- V_Prove checks body-satisfaction proofs and shared lemmas, plus protocol edge checks for open libraries, revising affected specifications and proofs when attempts expose semantic gaps.Dependency and coverage audits include admitted holes and used axioms; proof success remains relative to disclosed specifications and assumptions.Source: §5.4 · p. 13
5.5 Trust and Assurance Boundaries
- The guarantee depends on the Rocq kernel, VST and CompCert Clight semantics, the configured preprocessing path, correctness-critical gates, and disclosed premises.The LLM is outside the trusted computing base, while human conformance review remains an explicit assurance boundary; extending the guarantee to an executable requires downstream verified compilation.Source: §5.5 · pp. 13–14
6 EVALUATION
The evaluation verifies six C programs spanning data structures and openHiTLS cryptographic components. All 299 function bodies receive machine-checked proofs of memory safety and leak freedom under disclosed contracts and assumptions, with reported human effort below one person-day per benchmark.
Benchmarks and results
- The six programs cover pointer-based data structures and openHiTLS cryptographic components across 18 translation units.The cases include red–black tree and linked-list programs, plus ML-DSA and SLH-DSA signatures, SHA-256/224 hashing, and FrodoKEM key encapsulation; functions outside the listed cryptographic modules use disclosed external specifications.Source: §6 · p. 14
Results
- All 299 function bodies have machine-checked proofs of memory safety and leak freedom under their preconditions and stated external specifications; all six cases pass the no-admitted-obligations gate.Four libraries also include interface protocols, per-edge subsumption proofs, and a covering witness; functional correctness of the cryptographic algorithms, termination, and concurrency are outside the reported scope.Source: §6 · p. 14
Verification cost
- Human effort was reported as less than one person-day for each benchmark.Recorded elapsed time includes interruptions and service delays; for FrodoKEM, 17.03 total days included 193.1 hours of confirmed model-service downtime, yielding 8.99 days after subtraction.Source: §6 · pp. 14–15
Conformance review in practice
- Review of SHA-256/224 identified a self-copy call excluded by the generated contract, exposing a library defect for investigation and disclosure.CopyCtx(ctx, ctx) reaches memcpy with overlapping source and destination; the proof remains valid because its precondition requires disjoint resources.Source: §6 · p. 15
7 RELATED WORK
CCV builds on existing resource-aware verification and behavioral-interface methods rather than claiming those ideas as new. Its distinction is integrating a human-reviewed resource protocol with provider proofs and assurance review, alongside specification construction and proof automation in a codebase-level workflow.
7.1 Resource-Aware API Models and Behavioral Interfaces
- CCV organizes exported API contracts into a central reviewable protocol and connects it to provider-body proofs and accepted-run closure.VST specifications and ownership-aware systems already support resource-transforming interfaces; CCV builds on those semantic ingredients rather than claiming them as novel.Source: §7.1 · p. 15
- CCV’s protocol is design-shaped, interpreted by separation-logic resources, and exposed for human conformance review, rather than an inferred maximal implementation-safe language.Its contribution is integrating this reviewed protocol layer into assurance for verified C libraries, not a general theory of typestate or behavioral-interface synthesis.Source: §7.1 · p. 15
7.2 Automating Deductive Verification: ITP, Auto-active, and LLM-Based Approaches
- Prior automation often proves given specifications one goal at a time, while specification generators propose contracts or invariants without connecting them to intended design.Verifier acceptance alone does not establish that a generated specification is correct or complete with respect to design intent.Source: §7.2 · pp. 15–16
- CCV combines caller-driven contract analysis with kernel-checked separation-logic proofs and designated human review of artifact conformance.Unlike caller-driven approaches whose evidence stops at bug findings or bounded verdicts, CCV records and reviews propagated demands before delivering proved specifications.Source: §7.2 · pp. 16–17
8 CONCLUSION
CCV builds auditable assurance cases connecting machine-checked program proofs to intended requirements. Across six C benchmarks, it verifies memory safety and leak freedom for 299 function definitions with less than one person-day of reported human effort per benchmark, while retaining explicit human conformance review.
8 CONCLUSION
- CCV’s two-phase method co-evolves function specifications and proofs, while an interface protocol models intended cross-interface use and guides composable contracts.The protocol supports intended call sequences across library interfaces.Source: §8 · p. 17
- 299 function definitions across six C benchmarks receive memory-safety and leak-freedom proofs under disclosed contracts and assumptions.The benchmarks include industrial cryptographic components, and each required less than one person-day of reported human effort.Source: §8 · p. 17
- The assurance cases combine automated evidence construction with explicit human conformance review.Human review connects the formal artifacts to intended requirements.Source: §8 · p. 17