Authors Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, and Zhenjiang Hu introduce C*, a proof-integrated language design for C programming. C* extends C with verification capabilities powered by a symbolic execution engine and an LCF-style proof kernel. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code, facilitating interactive updates to the current proof state.

Its expressive and extensible proof support allows users to build reusable libraries of logical definitions, theorems, and programmable proof automation. Crucially, C* unifies implementation and proof code development by using C as the common language. The team implemented a prototype and evaluated it on a representative benchmark of small C programs and a challenging real-world case study: the attach function of p KVM's buddy allocator.

Results demonstrate that C* supports verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real-world scenarios.