CStar: Unifying Programming and Verification in C

The following summary was generated by AI from the slides.

CStar is a C-based language that unifies program implementation, specification, and proof in a single artifact, addressing two gaps in existing tools: lack of proof encapsulation across library boundaries and the inability to programmatically construct proofs using the full host language. It adopts a language-agnostic variant of the LCF architecture implemented via process separation, a QCP-backed symbolic executor for separation-logic reasoning, and program-proof states that couple verification conditions directly to program points. Users can write tactics, integrate SMT solvers, and build proof libraries entirely in C, with clang/clangd reused for compilation and IDE support.