C*: Unifying Programming and Verification in C
Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, Zhenjiang Hu
cs.PL, cs.SE
2025-04-03
C* puts a HOL Light kernel in C so proofs are C. Ten small programs plus pKVM attach_page verify; that function needs 1,616 proof lines for 57 lines of C.
Verifying systems C is still specialist work. One family of tools translates C into Coq (VST, AutoCorres, Live Verification). Programmers then prove properties in a language that looks nothing like C. Another family puts assertions or refinement types back into the C file (Frama-C, VST-A, RefinedC, CN). When the checker stalls, the work still drops into Coq. VeriFast lets you write a fixed set of proof commands and ghost lemmas, and you cannot grow that language.
C, from Peking University and Shanghai Jiao Tong University, tries to keep three properties at once: verification lives in the C source, proofs are as expressive as higher-order logic, and the current symbolic state is visible while you write the next line. The intended user is someone who writes kernels and allocators, not a theorem-proving expert.
C stacks two existing techniques on C: forward symbolic execution in separation logic, and an LCF-style proof kernel for higher-order logic. The kernel is HOL Light's OCaml core, reused rather than rewritten in C. Separation logic is axiomatized inside HOL Light, with the heap as a finite map from addresses to bytes; integers and pointers are the same sort in the object logic.
Specs are C attributes. Preconditions go in [[require]], postconditions in [[ensure]], loop invariants in [[invariant]]. Separation-logic predicates inside those attributes are quotations, and they are first-class C values of type term (object-logic type hprop). The standard library supplies maps-to predicates such as dataat and arrayat. Users can define inductive types and representation predicates, for example llrepr(p, l) tying a linked-list pointer to a logical integer list.
Proofs live in [[proof]] blocks, which are ordinary C. A block reads the current symbolic heap with getsymbolicstate(), rewrites it with a proved entailment, and writes it back with setsymbolicstate(). The engine has a hard rule: before a load or store, a primitive dataat or undefdataat for that address must already sit in the symbolic heap as a separating conjunct. If it does not, you write proof code that splits arrays or unfolds user predicates until the engine can see the cell. In the clear example, the loop invariant only says "the suffix is an uninitialized array"; the helper singleoutlocation peels off the head cell before the store.
That split gives two styles. Declarative: assert a desired state, let the engine emit verification conditions, prove them later. Operational: rewrite the symbolic state on the spot, interleaved with symbolic execution. That interleaving is what they call real-time verification. At deploy time the annotations are C attributes, so gcc or clang compiles the program and ignores the proof blocks.
Proof checking has three stages. The compiler slices the implementation at proof-block boundaries. An operational proof program feeds those slices to the symbolic-execution engine and runs the blocks. A residual proof program discharges leftover verification conditions. The library function localapply does the tedious structural work: lift the affected conjunct, apply the frame, put existentials back. A proof rule is just a C function that returns a thm, so experts can ship libraries.
The evaluation is ten small programs plus one real case. Most small examples are adapted from the VeriFast repository; the buddy-allocator example comes from CN; a few were written to stress control flow.
| Program | Impl. lines | Proof blocks | VCs | Proof lines | Spec/assert lines |
| swap | 15 | 0 | 0 | 0 | 7 |
| mallocfree | 9 | 1 | 0 | 9 | 8 |
| clear | 9 | 7 | 0 | 120 | 11 |
| reverse | 18 | 7 | 1 | 375 | 58 |
| attachpage | 57 | 6 | 3 | 1616 | 451 |
swap goes through with a purely declarative proof and zero proof lines. clear pairs 9 lines of C with 120 lines of proof. In-place list reverse needs 375 proof lines, plus four logic lemmas and two ownership lemmas that can be reused. The realistic case is attachpage from Android pKVM's buddy allocator: 57 lines of implementation, 451 lines of spec, 1,616 lines of proof. That is about 28x proof and 8x spec relative to the C. During the proof they found CN's original spec too weak to conclude that every free block sits in a doubly linked list, and they kept that weaker spec.
Covered C features include multi-way branches, mutual recursion, break/continue/early return, globals, address-taken locals, multi-level pointers, and malloc/free. Unsupported: switch, goto, for, and do-while. Two undergraduates carried out the evaluation.
For people writing kernels, hypervisors, and allocators, the pitch is that the proof language is C. Live Verification also aims at proving as you type, but the scripts are Coq Ltac, a different muscle memory. VeriFast automates more, with a closed command set. C bets extensibility on "a proof rule is a C function," so experts can package libraries for ordinary programmers.
It is not a production tool yet. There is no IDE that shows the symbolic state next to the code, no SMT backend for trivial facts, and a lot of boilerplate for heap reshaping. Those three complaints come from the undergraduates who used it. Treat it as a language-design prototype: if proofs can be written in C, will systems programmers verify their own code?
The prototype does not match the ideal workflow drawn in the paper. The authors cannot reach the external symbolic-execution engine's internal state, so each proof block currently requires running the engine twice by hand, once to read the heap and once to write it back. That is some distance from "see the heap after every line."
The trusted base includes the symbolic-execution engine, the HOL Light kernel, and the separation-logic axioms. Proof programs are C; the kernel is OCaml, glued through an interface.
The evaluation is small. attachpage is one function, not the whole allocator. There is no head-to-head comparison of proof size or person-time against VeriFast, CN, or VST on the same programs, and no reported checking times. The missing C features are common in systems code. Z3/Why3, an IDE, and a richer proof library are listed as future work.