C语言代码即证明：边写边验证
推荐指数 66.0 NO. 010 · 2026.09.09
发布2026/09/08Score52Comments33
为什么值得看
C* 是一种将 C 语言编程与形式化验证统一的新语言，程序员在写代码的同时即可完成证明，无需切换工具链。对需要高可靠性但受限于验证成本的基础设施团队有直接价值。
编辑判断
形式化验证领域长期被 Coq、Isabelle 这类交互式证明工具主导，程序员和验证工程师基本是两套人马，沟通成本极高。C* 的核心思路是把验证逻辑直接嵌入 C 语法层，类似 Rust 的所有权检查器但针对更广义的安全属性。
不过要注意，这类"统一"尝试前有先例：Microsoft 的 VCC 和 MIT 的 Bedrock 都做过类似探索，但都没走出学术圈。C* 能否突破取决于它处理 C 指针别名和内存模型的实际复杂度，以及编译到可执行代码的性能损耗。论文提到有原型实现，建议关注后续是否开源和实际代码规模下的验证时间。
做操作系统、数据库存储引擎或嵌入式固件的团队可以跟踪，如果验证开销能控制在 2-3 倍开发时间内，对安全关键场景的商业化路径会很清晰。
社区反馈
意见分歧 29 条评论
核心争论：形式化验证语言的语法可读性与实用价值之争
The "C*" language website - https://cstarlang.org/en/intro.html See in particular, usage benefits with LLMs (last para of https://cstarlang.org/en/intro.html) and how to use it with LLMs (https://cstarlang.org/en/tutorial/cstar-mcp.htm
Great idea, terrible syntax.
What's terrible about the syntax? Using "[[require/ensure/invariant/proof/assert/etc.]]" is actually pretty neat. And given that almost all C programmers are also C++ programmers, no mere syntax can faze us :-)