一份提交于2025年4月3日的arXiv论文（编号2504.02246）公布了一种新的编程语言原型——C\*，目标是让写C代码和写验证证明变成同一件事，用同一套语法、同一个文件完成。
核心判断是：这套东西目前只在一批小型C程序和pKVM内存分配器的一个函数上跑通，证明了"用C语言自己写证明"这条路走得通，但离替代现有验证工具、覆盖完整C语言或验证整个操作系统内核，还有相当距离。
一个函数的验证：C*做了什么
C*给C语言加了一种新代码块——proof-code，工程师可以把证明代码直接写在实现代码旁边。背后驱动的是符号执行引擎和一个LCF风格的证明内核：前者跟踪程序运行状态，后者保证每一步推理都有逻辑依据，不能凭感觉跳步。程序员还能像攒代码库一样，积累可复用的定理库和证明自动化脚本。
论文的评测分两块：一批有代表性的小型C程序基准，以及一个更硬的真实案例——pKVM（一款ARM架构轻量级hypervisor）内存分配器里的buddy allocator attach函数。作者称C*成功处理了这个函数里复杂的推理任务。
要澄清一点：验证通过的是attach这一个函数，不是整个buddy allocator，更不是整个pKVM。论文摘要没有给出通过率、耗时或代码行数这类量化数据，读者不必脑补出"pKVM已被形式化验证"这种结论。
分工的变化：把证明搬进程序员的编辑器
现在做C代码形式化验证，主流工具比如Frama-C和VeriFast，通常把验证当成独立环节：程序员先写完实现，再切换到另一套语法、另一套工具链去写规格和证明，证明失败了还要跳回去改代码。论文把这个问题点得很直接——环境和范式的割裂，是普通程序员不参与验证的关键障碍。
C*的解法是让证明代码和实现代码用同一种语言、同一个文件、同一个开发环境写。
C*的卖点不是证明能力更强，而是让证明变得顺手
这不是什么惊天创新，更接近把验证往"轻量化"和"日常化"方向推一步——类似单元测试从独立QA环节变成开发者随手写的东西。对内核、嵌入式和安全关键系统团队来说，这个方向如果成立，意味着形式化验证有可能从少数专家的专属工作，变成普通工程师日常代码评审的一部分。但工具链成熟、教学成本和生态积累，不是一篇论文能解决的事。
边界：原型阶段的证据有多厚
论文本身只是一个原型（prototype）的评测，证据分量有限。它证明了两件事：C能处理一批小程序，也能处理一个真实内核函数。这两件事值得肯定，但离"C能验证生产级系统软件"还有很长距离——支持的C子集有多大、证明一个函数平均要花多少人力、维护成本随代码规模怎么涨，论文摘要都没给出可比数据。
- 风险.目前的证据仅覆盖小样本基准和单个函数，不能反推C*已具备工业级验证能力
对准备评估形式化验证工具的团队来说，C现在更适合当作一个值得跟踪的研究方向，而不是可以立刻拿去替换Frama-C或VeriFast的现成选项。下一步该看的是：有没有后续版本给出更大规模的评测，以及是否有团队在真实项目里试用C，而不只是学术案例。