C*: Unifying Programming and Verification in C

Researchers have introduced C*, a proof-integrated language that extends C with built-in verification capabilities, allowing programmers to embed proof code alongside implementation code for real-time verification. C* uses a symbolic execution engine and LCF-style proof kernel to unify programming and verification practices in a single C-based environment, addressing the accessibility gap that typically keeps conventional programmers disconnected from formal verification. The prototype was tested on benchmark programs and a real-world case study of pKVM's buddy allocator, demonstrating its ability to handle both standard C idioms and complex verification tasks.