C*: Unifying Programming and Verification in C

C* extends C with embedded verification, integrating a symbolic execution engine and an LCF-style proof kernel. Programmers interleave proof-code blocks with implementation, allowing real-time proof state updates. The system supports reusable libraries of logical definitions and theorems. Prototype tests on small C programs and pKVM’s buddy allocator’s attach function demonstrate verification of many C idioms. C* handles complex real-world reasoning tasks effectively.