引言

作为信息系统的基石，操作系统、编译器、虚拟机、数据库等系统软件，构筑起整个数字社会的运行底座。 这类软件一旦出现故障，往往会引发灾难性后果。 近年来，从云服务大面积瘫痪到操作系统突发崩溃，各类故障屡见不鲜，带来了惨重的经济损失与社会秩序混乱。 保障系统软件安全稳定，早已不是锦上添花，而是数字时代必须守住的基本防线。

在各种安全保障手段中，类型系统、静态分析、动态测试、模型检查各有所长，但都只能覆盖特定类型的问题，难以从整体上杜绝缺陷。 形式化证明为此提供了更坚实的安全保障：依托严谨的数学推理，可证明程序在任意场景下都能符合设计规约，根除实现环节的缺陷。 例如，经过形式化证明的微内核 seL4，被部署于 DARPA 军用无人直升机等高安全场景，被广泛视为安全操作系统的标杆之一； 经过形式化证明的 C 编译器 CompCert，在大规模测试中未发现任何实现错误，已被空客等航空企业应用于安全攸关的飞控软件开发中。

遗憾的是，形式化证明至今仍是业内少数专家才能驾驭的 “技术奢侈品”。问题根源并非证明技术能力不足，而在于开发与证明的相互割裂： 就拿最常用的 C 语言来说，开发者基于命令式风格完成编码，证明工作却要在 Isabelle/HOL、Rocq（原 Coq）等基于函数式语言的证明助手中进行， 意味着要切换语言、工具与思维方式，从零构建证明过程。 以 seL4 内核为例，仅需约两人年即可完成的内核实现，对应的形式化证明却耗费近二十人年，证明成本是开发工作的十倍。 开发与证明环节彼此脱节，正是形式化证明难以普及、无法融入普通程序员日常工作的根本阻碍。

我们认为，突破这一困境的思路，并非让开发者适应现有证明工具，而是反其道而行之：直接将形式化证明能力原生融入开发者熟知的编程语言。 让开发与验证共用同一种语言、同一个环境、同一套工作流程，二者深度融合。 我们将这套理念称作开发与证明一体化，并基于该思路研发了一个面向 C 程序验证的系统编程语言 C*。

这一想法，基于一项至关重要的观察：编写程序与构造证明在本质上属于同一种活动。 受柯里-霍华德对应启发，我们在以 C 为代表的命令式编程范式下注意到，程序代码描述的是“程序状态”如何随语句的执行逐步变迁； 而一段证明刻画的则是“证明状态”——包括已确立的引理与当前待证目标——如何随推理的推进逐步演进。 既然二者皆为围绕状态的命令式演算，我们完全可以采用同样的 C 语法，在同一份源码中紧密耦合实现与证明。

已有的程序验证工具大致分布在两极。 一极以证明助手为中心，典型代表如 seL4 所采用的 Isabelle/HOL、CompCert 所采用的 Rocq，以及 VST、Iris 等框架，这类工具具备极强的表达能力， 但学习与使用门槛高，只有少数专家能够驾驭，同时还存在开发语言与证明语言相互割裂的问题。 另一极以自动化为中心，如 Dafny、Verus、Frama‑C、VeriFast、CN，这类工具上手容易，但表达力和可扩展性受限，一旦超出 SMT 等自动求解器的能力边界， 要么工具会失效或难以调试，要么需切换至独立的证明环境继续工作。 除此之外，像 F*、ATS、Idris、Lean 这类语言在函数式范式中实现了程序与证明的融合，却与系统软件开发实践中主流的命令式编程风格并不契合。 C* 兼具两极之长：沿用 C 语言的命令式范式，在语言层面直接集成完整的证明能力（而不止于自动求解），再辅以实时反馈和可调试的规约——既追求证明的表达力，也追求开发的易用性。

为了直观展示 C* 语言，我们以经典的原地反转单向链表的 C 实现为例。先来回顾下其具体实现代码：

struct list {
  int head;
  struct list *tail;
};
struct list *reverse(struct list *pt) {
  struct list *ret = NULL;
  while (pt) {
    struct list *nxt = pt->tail;  // 暂存后继
    pt->tail = ret;               // 反转指向
    ret = pt;                     // 前移已反转段
    pt = nxt;                     // 前移待处理段
  }
  return ret;
}

struct list {
  int head;
  struct list *tail;
};
struct list *reverse(struct list *pt) {
  struct list *ret = NULL;
  while (pt) {
    struct list *nxt = pt->tail;  // 暂存后继
    pt->tail = ret;               // 反转指向
    ret = pt;                     // 前移已反转段
    pt = nxt;                     // 前移待处理段
  }
  return ret;
}

这个程序虽简单，要证明它正确——返回值确实是输入链表的反转——却需要精确刻画每一步如何改变内存。 在 C* 里，规约和证明不写在别处，而是直接嵌入同一份 C 源码中，且都可以使用 C 语法（例如函数调用表达式）书写：

struct list *reverse(struct list *pt)
  [[cst::param(mk_var("l", mk_list_type(mk_int_type())))]]
  // 幽灵参数: 链表的逻辑内容 l
  [[cst::require(`sll pt l`)]]
  // 前置: pt 指向内容为 l 的链表
  [[cst::ensure(`sll __return (REVERSE l)`)]]
  // 后置: 返回值指向内容为 REVERSE l 的链表
{
  struct list *ret = 0;
  [[cst::proof]] fold_sll_null(`0i`);            // 空指针即空链表
  while (pt)
    [[cst::invariant(`exists l1 l2 pt_v ret_v.
        fact(l == REVERSE l1 ++ l2) **
        data_at pt__addr Tptr pt_v ** data_at ret__addr Tptr ret_v **
        sll ret_v l1 ** sll pt_v l2`)]]
  {
    [[cst::proof]] unfold_sll_not_null(`pt_v`);  // 打开链表头, 显式得到 tail 的所有权
    struct list *nxt = pt->tail;
    pt->tail = ret; ret = pt; pt = nxt;
    [[cst::proof]] fold_sll_not_null(`pt_v`);    // 折回 ret 一侧的链表
    [[cst::proof]] assert_by_rewrite(            // 用列表理论把证明不变式保持
      `l == REVERSE (h :: l1) ++ t`,
      ThmList(REVERSE_DEF, APPEND_DEF)
    );
  }
  return ret;
}

struct list *reverse(struct list *pt)
  [[cst::param(mk_var("l", mk_list_type(mk_int_type())))]]
  // 幽灵参数: 链表的逻辑内容 l
  [[cst::require(`sll pt l`)]]
  // 前置: pt 指向内容为 l 的链表
  [[cst::ensure(`sll __return (REVERSE l)`)]]
  // 后置: 返回值指向内容为 REVERSE l 的链表
{
  struct list *ret = 0;
  [[cst::proof]] fold_sll_null(`0i`);            // 空指针即空链表
  while (pt)
    [[cst::invariant(`exists l1 l2 pt_v ret_v.
        fact(l == REVERSE l1 ++ l2) **
        data_at pt__addr Tptr pt_v ** data_at ret__addr Tptr ret_v **
        sll ret_v l1 ** sll pt_v l2`)]]
  {
    [[cst::proof]] unfold_sll_not_null(`pt_v`);  // 打开链表头, 显式得到 tail 的所有权
    struct list *nxt = pt->tail;
    pt->tail = ret; ret = pt; pt = nxt;
    [[cst::proof]] fold_sll_not_null(`pt_v`);    // 折回 ret 一侧的链表
    [[cst::proof]] assert_by_rewrite(            // 用列表理论把证明不变式保持
      `l == REVERSE (h :: l1) ++ t`,
      ThmList(REVERSE_DEF, APPEND_DEF)
    );
  }
  return ret;
}

在 C* 中，程序安全性与正确性的证明在分离逻辑（一种擅长描述指针与内存所有权的逻辑）中进行。 语法层面上，反引号 `...``...` 里是逻辑断言，sll pt lsll pt l 的含义是“指针 ptpt 指向内容为列表 ll 的单向链表”， ****（分离合取）连接两块不相交的内存区域，data_at a Tptr vdata_at a Tptr v 表示地址 aa 处保存着指针值 vv， REVERSEREVERSE、++++ 是从已有列表理论直接复用的逻辑函数（反转、拼接），__return__return 指返回值，__addr__addr 表示变量 的地址。 围绕它们，C* 提供三类标注：[[cst::require(...)]][[cst::require(...)]] / [[cst::ensure(...)]][[cst::ensure(...)]]（连同幽灵参数 [[cst::param(...)]][[cst::param(...)]]）声明函数契约， [[cst::invariant(...)]][[cst::invariant(...)]] 声明循环不变式，[[cst::proof]] ...[[cst::proof]] ... 在程序中嵌入证明代码。 例如循环体里的 unfold_sll_not_nullunfold_sll_not_null（一个 C* 函数）把非空链表的头节点打开，显式地获得 tailtail 字段的所有权，紧接着的 pt->tailpt->tail 读写才合法； assert_by_rewriteassert_by_rewrite（另一个 C* 函数）则用列表理论的等式定律，证明不变式在循环中保持成立。 包括契约中使用的 mk_varmk_var、mk_list_typemk_list_type、mk_int_typemk_int_type 在内的上述 C* 函数本身也是普通 C 代码， 所以它们可以如同软件工程一般进行证明工程，例如构建可复用的证明代码库。

在 C* 编程环境中，开发与证明是同步且实时的。例如，当执行到循环体入口时，环境中可以实时显示此处的符号状态：

它给出程序此刻的精确符号状态：存在已反转段 l1l1 与剩余段 l2l2，满足 l == REVERSE l1 ++ l2l == REVERSE l1 ++ l2； retret 指向拥有内容 l1l1 的链表，ptpt 指向拥有内容 l2l2 的链表，二者互不相交。 每写一行代码，这个符号状态也会相应更新；若某步缺少所有权，C* 会实时报错，例如未先 unfoldunfold 就访问 pt->tailpt->tail， 会得到“无法推出内存访问的前置条件”。 写完一个函数后，若缺少循环不变式或后置条件的证明，C* 会在相应的位置报告待证明的验证条件。

C* 不仅在程序设计语言、编程环境与工作流程层面实现了开发与证明的深度融合，还开启了下述两个新的研究方向。

其一，可编程的验证自动化。 我们正以“定理证明器”架构的视角重新审视“程序验证器”的架构：将验证过程中的各种自动化策略本身打造为可复用、可组合的证明代码库， 由开发者按需扩展，而无需将这些策略纳入可信计算基。 这一思路同样可延伸到程序分析领域：编写断言、循环不变式等规约标注是验证中最繁琐的一环。 为此，我们可以将指针别名分析、不变式推断等成熟的程序分析技术也实现为同样的证明代码库，使其与验证流程紧密协作，自动生成规约标注以降低人工负担。 更为重要的是，分析结果可被证明内核检查，由于分析模块不必位于可信计算基之中，即便分析器出错也不会导致伪证。 这让程序分析、类型系统等与形式化证明融为一体，既拥有自动化工具的便捷，又不牺牲可信性。

其二，面向智能体的可信编程。 大模型正在改变软件开发，但“人工智能写的代码到底对不对” 始终悬而未决。 将大模型和形式化证明相结合，大模型解决形式化证明的高成本，形式化证明给大模型编写的程序给出安全保障，已经成为学界和业界共同努力的方向。 相比现有形式化证明语言，C* 更加适配大模型： (1) 大模型在跳转和读取大量文件时容易出错，C* 的设计让程序和证明在同一个位置，完成任务时无需大量跳转，相比开发和证明分离的语言更适合大模型使用； (2) 基于 SMT 求解的语言往往只能给出弱反馈且多次执行不稳定，C* 对于证明和普通 C 语句都维护统一、稳定的符号状态， 可更好地指导大模型编写和修改代码，避免在出错时受阻。我们正从数据、训练到环境设计，为 C* 打造这样一个“会写代码也会写证明” 的智能体。

这些探索最终都指向形式化证明在产业中的落地：把 C* 用于操作系统内核、网络协议实现等系统软件的验证，沉淀可复用的高安全代码库； 也包括把程序验证的教学门槛，从需要博士功底，逐步降到本科生也能掌握，让更多人真正用得上形式化证明。