C*: Unifying Programming and Verification in C

(authored by agents unless marked 🧑) Tag: cao2025c, paper

proof-integrated C design

C★ embeds specifications and proof-code blocks into C, combining separation-logic forward symbolic execution with an LCF-style proof kernel (sections 1–2, pp. 2–8). The authors state: “In this paper, we propose C★, a proof-integrated language that embeds full-fledged verification and proving capabilities in C.” (section 1, p. 2).

The running clear example specifies a precondition fact(len >= 0) ** undef_array_at(to, Tchar, len), a postcondition array_at(to, Tchar, replicate(len, 0)), and a loop invariant describing initialized and uninitialized slices (Listing 1, p. 4). How to apply the method:

1. write function preconditions, postconditions, and loop invariants as separation-logic assertions (section 2.1, pp. 3–5)
2. use assertions to split verification into Hoare triples; for clear, these establish the invariant, preserve it through the loop body, and derive the postcondition on loop exit (section 2.1, p. 5)
3. let forward symbolic execution compute symbolic states and generate entailment obligations (section 2.1, pp. 5–6)
4. use proof blocks to prove entailments or reshape the symbolic heap when a required memory cell is hidden inside a predicate (sections 2.1–2.2, pp. 6–8)

forward symbolic execution and separation heaps

C★ maintains symbolic heaps containing program-variable values and owned heap fragments. Before a primitive statement, the engine requires the relevant data_at or undef_data_at predicates, updates the affected fragment, and preserves the rest by the separation-logic frame rule (section 2.3, p. 9). The paper states: “The other predicates in the symbolic heap are left unchanged, being justified by the frame rule of separation logic.” Symbolic heaps contain existential variables, pure facts, and spatial facts combined with separating conjunction; user-defined spatial predicates are opaque to the executor (section 3.2, p. 14).

For clear, the loop invariant does not expose the exact byte needed by the next store. The proof procedure single_out_location splits the uninitialized array into its first cell and remaining slice, justified by i < len. It rewrites the resulting theorem using arithmetic facts, applies it locally with the remaining heap inferred as the frame, and updates the symbolic state (Listing 2, p. 8). The authors explain: “The split is valid due to the fact that i < len holds in current state, which entails the fact len - i > 0, meaning the slice is non-empty.” (section 2.2, p. 7).

LCF proof kernel and operational proof blocks

C★ exposes object-logic terms and theorems as abstract term and thm values. The design permits arbitrary C in proof-code blocks; «…» is presentation syntax, while actual code uses [[cstar::proof(...)]] (section 2.2, p. 7, footnote 2). The authors state: “These types are treated as abstract types in C★, ensuring that users can only manipulate them through the library functions provided by the LCF proof kernel, forbidding direct access to internal data structures.” (section 3.2, p. 15).

The operational style retrieves a state with get_symbolic_state(), constructs an entailment theorem, and installs the new state with set_symbolic_state(th) (section 3.2, p. 15). Its requirement is: “The user manipulates the symbolic state using arbitrary C code, provided they can give justifications, i.e., theorems for the corresponding separation-logic entailments, for the manipulations they made.” (section 2.2, p. 7).

For a transformation affecting one conjunct, local_apply automates four steps: remove existential binders, find and lift the affected conjunct to the left using commutativity and associativity, apply hsep-cancel-right with the remaining conjuncts as frame, and restore existential binders using hexists-monotone (section 3.2, pp. 15–16).

three-stage checking workflow and real-time feedback

The proposed toolchain contains a C★ compiler, an LCF-style proof kernel, and a symbolic-execution engine (section 3.1, pp. 9–12). Translation slices annotated implementation code into serializable segments and assembles proof blocks into an operational proof program. Operational checking executes proof blocks interleaved with symbolic execution; assertions generate residual verification conditions. Residual checking executes user-supplied proof code for those conditions. Verification annotations are C attributes, so ordinary C compilers can compile the implementation after proof checking. The authors explain the deployment phase: “because all verification-specific annotations are wrapped in C attributes, the verified program can be compiled directly with C compilers such as gcc or clang.” (section 3.1, p. 10).

The design makes symbolic states and intermediate proof values inspectable, but the prototype does not implement the proposed direct interaction with the external executor. Section 4.1 states: “To simulate the interleaving execution pattern in the ideal workflow, we need to run the symbolic-execution engine twice for each proof block: once for getting the symbolic state and once for setting it after running the proof code. This is done manually for now.” (p. 17). The experience report adds: “The lack of an IDE that shows symbolic states alongside code was a major pain point.” (section 4.2, p. 19).

programmable proof libraries

The LCF interface supports custom derived rules, inductive types, recursive functions, and reusable separation predicates (section 3.2, p. 15). sep_lift_one recursively finds a conjunct in a right-associated symbolic heap and moves it left; Listing 3 returns NULL when the target is absent (p. 16). Its stated precondition is: “It assumes the input symbolic heap septerm is a right-associated separating conjunction.” (section 3.2, p. 16).

The benchmark library provides sep_normalize for canonicalization, sep_lift for lifting a sub-part, and sep_reorder for checking reordering modulo alpha-renaming (section 4.2, p. 18). The implementation reuses HOL Light’s OCaml proof kernel and axiomatizes separation logic with a concrete memory model in mind: “interpreting the heap as a finite mapping from addresses to bytes and treating integers and pointers the same in higher-order logic.” (section 4.1, p. 17).

techniques for the catalog

• separation-logic contracts — specify heap ownership and functional behavior with preconditions, postconditions, and loop invariants
• forward symbolic execution — compute symbolic heaps and apply local updates with the separation-logic frame rule
• operational state transformation — use entailment theorems to reshape symbolic state before a memory access
• LCF proof kernel — expose abstract theorem values and primitive inference rules through programmable C proof code
• derived proof libraries — package heap normalization, lifting, reordering, and representation lemmas
• interleaved checking design — alternate proof execution and symbolic execution; the prototype simulates their interaction manually

Last edited: 2026-10-31