C*: Unifying Programming and Verification in C

论文提出 proof-integrated 的 C*，让程序员在实现代码旁嵌入 proof-code，符号执行引擎负责状态推进，LCF 风格内核负责可信检查。原型覆盖小型 C 基准，并在 pKVM buddy allocator 的 `attach` 函数上处理复杂推理，说明目标不是只验证玩具循环。把证明和实现共用 C 语法降低了工具切换成本，但论文目前仍是原型和有限案例，离完整 C 生态的工程验证还有距离。