C*: Unifying Programming and Verification in C
Recorded: Sept. 8, 2026, 5:08 p.m.
| Original | Summarized |
[2504.02246] C*: Unifying Programming and Verification in C
Skip to main content Search Log in Search arXiv Press Enter to search · Advanced search Computer Science > Programming Languages arXiv:2504.02246 (cs) [Submitted on 3 Apr 2025] 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. Subjects: Programming Languages (cs.PL); Software Engineering (cs.SE) Cite as: Focus to learn more arXiv-issued DOI via DataCite Submission history From: Yiyuan Cao [view email] [v1]
Full-text links: View a PDF of the paper titled C*: Unifying Programming and Verification in C, by Yiyuan Cao and 10 other authorsView PDFHTML (experimental)TeX Source view license < prev | new Change to browse by: References & Citations NASA ADSGoogle Scholar export BibTeX citation BibTeX formatted citation loading... Data provided by: Bookmark
Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Code, Data and Media Associated with this Article alphaXiv Toggle alphaXiv (What is alphaXiv?) Links to Code Toggle CatalyzeX Code Finder for Papers (What is CatalyzeX?) DagsHub Toggle DagsHub (What is DagsHub?) GotitPub Toggle Gotit.pub (What is GotitPub?) Huggingface Toggle Hugging Face (What is Huggingface?) ScienceCast Toggle ScienceCast (What is ScienceCast?) Demos Demos Replicate Toggle Replicate (What is Replicate?) Spaces Toggle Hugging Face Spaces (What is Spaces?) Spaces Toggle TXYZ.AI (What is TXYZ.AI?) Related Papers Recommenders and Search Tools Link to Influence Flower Influence Flower (What are Influence Flowers?) Core recommender toggle CORE Recommender (What is CORE?) Author About arXivLabs arXivLabs: experimental projects with community collaborators Which authors of this paper are endorsers? | We gratefully acknowledge support from About Major funding support from |
The work introduces C*, a novel proof-integrated language design for the C programming language, aimed at unifying the processes of programming and formal verification. The motivation for this approach stems from the necessity of ensuring correctness in safety-critical and low-level systems software. Despite advancements in verification tooling, the involvement of conventional programmers in code verification remains limited, contributing to increased development and maintenance costs. A significant obstacle preventing broader participation in verification practices is the fundamental disconnect between programming paradigms and verification methodologies, which hinders accessibility and real-time verification capabilities. C* addresses this by extending C with integrated verification features, powered by a symbolic execution engine and an LCF-style proof kernel. This framework facilitates real-time verification by allowing programmers to embed proof-code blocks directly alongside the implementation code, enabling interactive updates to the current proof state as development progresses. The language design supports expressive and extensible proof systems, allowing users to construct reusable libraries of logical definitions, theorems, and programmable proof automation. A core principle of C* is the unification of implementation and proof code development, achieved by leveraging C as the common language for both aspects. The authors implemented a prototype showcasing C* and evaluated its efficacy through testing on a representative benchmark of small C programs, as well as a challenging real-world case study involving the attach function of pKVM's buddy allocator. The results demonstrated that C* is capable of verifying a wide range of C programming idioms and effectively manages complex reasoning tasks encountered in practical scenarios. This research establishes C* as a method for bridging the gap between software implementation and formal proof, thereby enhancing the ability of programmers to develop and maintain verified software artifacts. |