C* embeds machine-checked proofs inside C code to unify programming and verification

What the researchers built

A research team has proposed C*, an extension of the C language designed to let programmers write formal correctness proofs next to the code those proofs describe. The paper, submitted to arXiv in April 2025 by a group including Yiyuan Cao, Qinxiang Cao, Yingfei Xiong and Zhenjiang Hu, recently surfaced on the front page of Hacker News.

According to the paper, C* rests on two components. The first is a symbolic execution engine, which reasons about how a program behaves across possible executions rather than a single run. The second is an LCF-style proof kernel: a small, trusted core, in the tradition of established proof assistants, through which every theorem must pass before it is accepted. Together they let the environment check both what the code does and whether a stated property about it actually holds.

Why programmers skip verification

Formal verification is a long-standing goal in systems software, where low-level memory manipulation and safety-critical responsibilities make bugs expensive. Yet, as the authors observe, conventional programmers are rarely involved in verifying their own code, which pushes up the development and maintenance costs of verified software.

The barrier, according to the paper, is that programming and verification happen in disconnected environments and paradigms: the implementation lives in C and its toolchain, while proofs are typically developed elsewhere, in separate tools, on separate timelines. That separation limits accessibility and rules out real-time checking, so verification never becomes part of the normal edit-and-compile loop.

How C* blends the two

C*'s answer is to make C itself the common language for both activities. Programmers embed proof-code blocks alongside implementation code, and the prototype verifies them in real time, interactively updating the current proof state as work progresses. The intended experience is closer to a type checker or linter that responds as you type than to an after-the-fact audit by a separate team.

The proof support is also meant to be expressive and extensible. Users can build reusable libraries of logical definitions and theorems, and they can write programmable proof automation, so recurring reasoning patterns do not have to be reconstructed by hand for every new function or module.

What was evaluated

The authors implemented a prototype and tested it on two fronts. First, a benchmark of small C programs demonstrated, according to the paper, that C* can verify a broad subset of common C programming idioms. Second, as a demanding real-world case study, they verified the attach function of pKVM's buddy allocator, part of the memory-management machinery of the protected kernel virtual machine hypervisor. The authors report that C* coped with the complex reasoning that this piece of real systems code demanded.

Why it matters

Much of the world's safety-critical infrastructure — kernels, hypervisors, drivers, embedded controllers — is written in C, and almost none of it ships with machine-checked correctness guarantees. Software that does carry such guarantees has historically required dedicated verification expertise and separate tooling, which keeps the practice rare and costly.

C* points toward a different equilibrium: if proofs live in the same file, the same language and the same feedback loop as the implementation, verification could become a routine part of programming rather than a specialist discipline bolted on afterwards. The evidence is still early — a prototype, small benchmarks and one case study — and the paper does not claim production readiness. But the design direction, unifying programming and verification instead of bridging two disconnected worlds, is significant for anyone building systems software where correctness has to be argued, not merely tested.