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
TL;DR
C* addresses the costly separation between programming and formal verification by embedding full verification capabilities directly into C through forward symbolic execution and an LCF-style proof kernel. The approach enables real-time verification via proof-code blocks that programmers can interact with inside their normal code, while supporting extensible libraries of logical definitions and programmable proof automation. The authors implement a prototype toolchain and demonstrate its ability to verify a broad subset of C, including realistic cases such as a buddy allocator attach function, highlighting C*'s practical potential for verified systems software. Overall, C* offers a unified, programmable, and real-time verification framework that lowers the barrier for programmers to participate in formal verification and paves the way for broader adoption of verified C code.
Abstract
Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software. A key barrier to programmer participation in verification practices is the disconnect of environments and paradigms between programming and verification practices, which limits accessibility and real-time verification. We 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. We implemented a prototype of C* and evaluated it on a representative benchmark of small C programs and a challenging real-world case study: the attach function of pKVM's buddy allocator. Our results demonstrate that C* supports the verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real-world scenarios.