QCP 能验证什么：从一个排序函数说起

请 AI 写一个排序函数，输入 [3, 1, 2]，它返回 [1, 2, 3]。再试几组负数、重复数字和已经排好的数组，也没有暴露任何错误。但对于所有符合条件的输入，程序都能保留原来的全部元素吗？移动数据时，会不会发生越界访问？

在当前的软件工程实践中，工程师们通过设计不同的测试用例，运行程序并检查结果，以判断代码是否正确。但测试用例再多，也难以保证覆盖所有边缘情况（corner cases）。形式化验证（Formal Verification）则开辟了另一条道路：用严密的数学推理替代穷举测试。 对排序函数来说，就是证明对于所有满足输入条件的数组，结果都有序、元素没有增减，并且执行过程中的内存访问安全，无需逐一运行所有可能的输入。

QCP（Qualified C Programming）是一个面向 C 语言程序的形式化验证系统。 它基于分离逻辑描述程序的内存和数据，将 C 代码与规约转化为待证命题，再由自动化求解器和交互式定理证明器完成证明。AI 可以辅助编写规约、标注和证明，生成的内容交由工具检查。

排序正确，究竟是什么意思？

要让计算机证明一个程序是正确的，第一步必须明确：什么叫“正确”？

对于 [3, 1, 2]，正确结果是 [1, 2, 3]。但若仅仅要求“输出数组从小到大排列”，还远远不够：返回 [0, 0, 0] 同样从小到大，却显然违背了排序的本意。因此，排序的正确性必须同时包含两个方面：

• 有序性（Order）： 数组中的前一个元素不大于后一个元素。
• 元素保持（Permutation）： 结果数组是原数组的一个排列，每个数字出现的频次严格相同，不可凭空增加、丢失或篡改元素。

此外，在 C 语言中，程序不仅要保证逻辑正确，还必须保证底层物理内存的安全：数组指针必须合法且具备读写权限，排序过程绝不能发生缓冲区溢出，也不能与其他变量发生未经声明的内存踩踏。

把调用前后的这些契约合并，便构成了规约（Specification）：

前置条件（Precondition）： 调用前，输入一段长度合法、具备独占读写权限的整数数组。
后置条件（Postcondition）： 函数返回时，数组完全有序，所有元素及其出现频次保持不变，且合法写回了结果。

形式化验证工具的任务，就是通过数学证明建立这份保证：在满足前置条件的情况下，函数返回时必然满足后置条件。

用 QCP 验证一个插入排序

插入排序是一种非常简单的排序算法，就像整理手中的扑克牌：左手持有的牌始终排好序，右手每次从无序区抽取一张牌，在有序区中自右向左找到合适位置并插入。对于 [3, 1, 2]，其状态演化如下（竖线左边为有序区）：

[3 | 1, 2]   →   [1, 3 | 2]   →   [1, 2, 3 |]

下面是一个插入排序实现：

void insertion_sort(int *nums, int numsSize) {
    for (int i = 1; i < numsSize; ++i) {
        int key = nums[i];
        int j = i - 1;
        while (j >= 0 && nums[j] > key) {
            nums[j + 1] = nums[j];
            j--;
        }
        nums[j + 1] = key;
    }
}

外层循环逐步扩大有序前缀；内层循环把比暂存值 key 大的元素逐个右移，为 key 腾出空位，最后归位。这短短几行代码，在形式化验证的世界里需要经历三道关键工序。

第一步：把排序要求写成规约

在 QCP 中，函数规约以特殊形式的注释 /*@ ... */ 直接内嵌在 C 代码中。下面是该排序函数的规约：

void insertion_sort(int *nums, int numsSize)
/*@ With (l: list Z)
    Require 1 <= numsSize && numsSize <= 50000 &&
            IntArray::full(nums, numsSize, l)
    Ensure exists l1,
           Permutation(l, l1) && increasing(l1) &&
           IntArray::full(nums, numsSize, l1)
*/

这份规约体现了 QCP 的两个核心设计洞见：

• 分离逻辑（Separation Logic）与内存解耦： IntArray::full(nums, numsSize, l) 描述这段数组的内容和读写权限。函数只需围绕这段内存完成证明；调用者还有其他不相交的内存时，可以用分离合取 A * B 将它们与数组分开描述，并在函数调用后保留未被修改部分的性质。这里的 * 表示两部分占有的内存互不重叠。
• 数据抽象（Data Abstraction）：从 C 指针到纯数学对象： 谓词 IntArray::full(nums, numsSize, l) 是现实物理内存与纯数学世界的桥梁。它表明指针 nums 处存储着一段长度为 numsSize 的有效 C 整数数组，其内容对应纯逻辑列表 l : list Z。随后，排序的业务逻辑直接使用纯数学命题陈述：Permutation(l, l1)（排列保持）与 increasing(l1)（非降序，允许相邻元素相等）。

第二步：说明每轮循环保持什么

证明循环时，不必把每一轮都展开。我们先说明程序每次执行到循环条件处时，哪些事实应当成立，再证明两件事：第一次到达这里时，这些事实成立；如果某一轮开始时成立，执行这一轮后仍然成立。这样，无论循环执行多少轮，都可以用同一个推理说明它的行为。这些事实称为循环不变量。

外层循环：已经处理的部分有序，元素没有改变。 每轮开始时，左边已经排好的部分包含原来这一段的全部元素，每个数出现的次数不变；右边尚未处理的部分保持原样。开始时左边只有一个数，自然有序。每完成一次插入，有序部分就增加一个元素；循环结束时，它覆盖整个数组。

内层循环：移动元素时，要把暂存的数一起算进去。 例如，将 2 插入已经排好的 1、3 之间，程序先保存 2，再把 3 向右移动。此时数组暂时变成 1、3、3，但 2 没有丢失，只是保存在变量中。统计数组中除待填位置以外的元素，再加上暂存的 2，原有元素及其次数仍然完整。

每向右移动一个数，待填位置就向左移动一格，已经移过的数都大于待插入的数。停止移动时，待填位置左边的数都不大于它；将它写回后，这一段便有序，数组中各元素的出现次数也保持不变。

/*@ Inv Assert
  exists l1,
    nums == nums@pre && numsSize == numsSize@pre &&
    1 <= i && i <= numsSize && numsSize <= 50000 &&
    Permutation(l, l1) &&
    (forall (p: Z) (q: Z), (0 <= p && p < q && q < i) => (l1[p] <= l1[q])) &&
    IntArray::full(nums, numsSize, l1)
*/

/*@ Inv Assert
  exists l1,
    nums == nums@pre && numsSize == numsSize@pre &&
    1 <= i && i < numsSize && numsSize <= 50000 &&
    -1 <= j && j < i &&
    INT_MIN <= key && key <= INT_MAX &&
    Permutation(l, replace_Znth(j + 1, key, l1)) &&
    (forall (p: Z) (q: Z), (0 <= p && p < q && q <= i && p != j + 1 && q != j + 1) => (l1[p] <= l1[q])) &&
    (forall (p: Z), (j + 1 < p && p <= i) => (key < l1[p])) &&
    IntArray::full(nums, numsSize, l1)
*/

第三步：让工具检查这些推理

有了规约与循环不变量，QCP 就可以进行符号执行（Symbolic Execution）：用符号表示输入，按程序语句推导各个位置应满足的条件，并在分支和循环处检查相应的推理。这个过程会生成一组待证明的命题，称为验证条件（Verification Conditions, VCs）。例如：

• 边界与安全条件： 读取 nums[j] 与写入 nums[j + 1] 时，下标是否严格落在 [0, numsSize) 内？当 j 递减到 -1 时，C 语言的短路求值（Short-circuit evaluation）能否确保不发生 nums[-1] 越界访问？
• 归纳建立与保持： 前置条件能否推出第一轮循环的不变式？单次循环体执行后，能否重新建立不变式？循环退出时，能否推出最终的后置条件？

QCP 自动处理内存关系，并将算术、等式等条件交给 SMT 求解器。其余条件导出到 Rocq（原 Coq）或 Lean 等交互式定理证明器中，由人或 AI 构造证明，再由内核按逻辑规则检查。当前代码和规约对应的全部验证条件通过后，才完成程序验证。

架构洞见：可信计算基（TCB）与工程实用主义
验证结果的可信性，取决于哪些组件必须被信任。VST（Verified Software Toolchain）在 Rocq 中建立 C 程序语义和分离逻辑证明，能够表达细粒度的正确性要求，也需要较多的证明工程。QCP 将适合自动处理的验证条件交给内置求解器，将其余条件交给交互式定理证明器，以减少需要显式构造的证明，同时支持复杂的算法性质。这个取舍也明确了它的可信计算基：符号执行与验证条件生成、自动求解器，以及所用定理证明器的内核。自动求解通过的条件依赖 QCP 求解器的正确性；补充构造的证明则由 Rocq 内核相对于所依赖的定义和假设检查。完整验证还需要确认验证条件对应当前源码与规约、补充证明没有遗漏，并核对所依赖的假设。

QCP 的证明边界

QCP 证明的是 C 源码满足规约。将这一结论用于实际运行，还需要编译器按照验证所采用的 C 语义正确编译，操作系统正确加载程序，硬件正确执行指令，调用的库满足接口规约。在这些前提下，对满足调用条件的输入，程序返回时就具有规约要求的性质。没有写入规约的其他要求，需要另行证明或检查。

AI 怎样参与这个过程？

长期以来，形式化验证之所以被视为“贵族软件工程”，一个原因是构造程序标注和证明需要大量专业工作。前面的排序例子中，除了说明最终结果，还要找到每轮循环应保持的事实，并完成相应推理。这些工作过去主要依赖人类专家和工程师完成，工作量大，人力成本也很高。现在，这些工作都可以由 AI 辅助完成。

AI 会写出错误的证明吗？

会，但错误的证明不会因此被接受。 QCP 和定理证明器会检查标注与证明，拒绝不符合证明规则的推理，并指出未通过的验证条件。AI 可以根据这些反馈继续修改，再交由工具检查。

规约确定后，AI 可以起草循环不变量、补充中间断言、编写 Rocq 或 Lean 证明脚本，再调用工具检查。未完成的验证条件和证明错误会成为下一轮修改的依据。

例如，如果内层循环的标注漏掉了暂存在 key 中的元素，就无法建立完整的元素保持关系。AI 需要修正对中间状态的描述，再重新检查相应的证明。仍未解决的问题需要人介入；如果修改涉及规约本身，也要交回人确认。

人确认要证明什么

形式化工具能证明代码符合规约，但不能判断规约是否符合人的真实意图。例如，删去排序的“元素保持”要求后，返回全零数组也可能满足剩下的要求。因此，人需要审核规约中的输入条件、输出要求，以及它们引用的定义，并确认实际使用场景满足这些输入条件。

人工审核可以减少到什么程度？

在完整验证通过、且信任验证工具链的前提下，为了确认规约描述的功能，人只需要审核规约及其依赖的定义，不需要再逐行审核实现代码和证明脚本。当一份较短的规约能够描述较大规模实现的功能时，人工需要阅读和判断的内容就可以相应减少。

“贵族软件工程”的成本，很大一部分来自构造和维护证明所需的专业工作。如果这些工作能更多地由 AI 完成，人集中审核需求和规约，形式化验证就有机会成为更多开发团队能够采用的工程方法。

从排序走向更复杂的程序

前面，我们通过排序的例子说明了规约、程序标注和证明如何配合。当程序规模增大、模块之间的依赖增多时，验证还要处理更复杂的控制流程、数据表示和接口关系。下面介绍 QCP 团队已经完成的几类验证工作。

一个 SAT 求解器说“无解”，我们为什么敢相信？

布尔可满足性（SAT）求解器是芯片验证、定理证明和安全分析的基础设施。事实上，现代 SAT 求解器为了追求极致的求解性能，在开发过程中加入了大量的优化策略。当求解器报告 SAT（有解）时，验证非常容易——只需将它给出的真值赋值代入公式即可。但当求解器报告 UNSAT（无解） 时，我们凭什么确信它没有因为复杂的底层指针 Bug 或回溯剪枝漏洞，而误删了一个真实存在的解？

例如，考虑下面的公式，其中 ∨、∧、¬ 分别表示“或”“且”“非”：

令 a、c、d 为真，b 为假，就能使每个子句都成立，因此这个公式是可满足的。求解器若返回这组赋值，我们可以直接代入公式，确认 SAT 结论。

如果把最后一个子句换成 ¬c ∨ ¬d，就得到：

前三个子句要求 a、b 至少一个为真，进而要求 c 为真；第四个子句又要求 d 为真，与最后一个子句矛盾。因此，这个公式不可满足。与检查一组满足赋值不同，确认 UNSAT 需要说明为什么所有可能的赋值都不成立。

QCP 团队与 AI 协作，完成了一个 C 语言 CDCL 求解器的功能正确性验证。我们证明的是：在输入满足规约的前提下，求解器若报告 SAT，保存的赋值就满足所求公式；若报告 UNSAT，所求公式就确实不存在满足赋值。

这里我们展示 CDCL 的验证结果。上述正确性要求写在入口函数 cdcl_solver 的规约中，下面摘录其主要结构，省略辅助参数：

int cdcl_solver(sat_data* s) /*@
  With (F : cnf) ...
  Require cnf_wf(n, F) && solver_input_core(s, F, ...)
  Ensure
    (exists J, __return == 1 && models(J, F) &&
      solver_sat_arm_core(s, F, ..., J)) ||
    (__return == 0 && cnf_unsat(n, F) &&
      solver_unsat_arm_core(s, F, ...)) ||
    (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, ...))
*/

Require 描述调用前的条件：F 是原始公式，n 是变量个数；公式中的变量编号需要合法，s 指向的数据结构需要正确存储公式，并满足初始状态和内存要求。

Ensure 描述返回时的保证。返回 1 时，models(J, F) 要求赋值 J 满足原始公式，solver_sat_arm_core 则将 J 与程序实际保存的赋值对应起来。返回 0 时，cnf_unsat(n, F) 要求原始公式不存在满足赋值。

这个实现还可能返回 -2，表示子句表容量耗尽，尚未得出求解结论。规约在这一分支保留对内存和数据结构的要求，不给出 SAT 或 UNSAT 判断，也不保证程序一定在容量耗尽前完成求解。

int cdcl_solver(sat_data* s )/*@ With (F : cnf) original_count (snap : dense_snapshot)
      (ranks : Z -> option nat) values reasons levels states true_counts unassigned
      row_table n live cap
    Require cnf_wf(n, F) &&
    solver_input_core(s, F, original_count, snap, ranks,
      values, reasons, levels, states, true_counts, unassigned, row_table, n, live, cap)
    Ensure
      (exists J, __return == 1 &&
      models(J, F) &&
        solver_sat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap, J)) ||
      (__return == 0 &&
      cnf_unsat(n, F) &&
        solver_unsat_arm_core(s, F, original_count, snap, ranks, values, reasons,
          levels, states, true_counts, unassigned, row_table, n, live, cap)) ||
      (__return == -2 &&
      solver_capacity_exhausted_arm_core(s, F, original_count,
        snap, ranks, values, reasons, levels, states, true_counts, unassigned,
        row_table, n, live, cap))
*/

模块化分层验证：从大整数底层算术到高层消元算法

在现实软件中，高层算法往往建立在底层基础设施之上。如何避免每次验证高层程序时都重新陷入底层的泥潭？模块化规约抽象（Modular Verification & Data Abstraction）是形式化验证的王牌。

在消元算法（如求解线性不等式的傅里叶–莫茨金消元与求解线性方程组的高斯消元）中，中间系数极易超出机器字长限制，必须依赖大整数库（如 mini-gmp）。然而，底层的多精度大整数乘法在 C 语言中涉及大量数位数组操作、进位传递与位运算，如果直接在算法验证过程中进行频繁的底层谓词展开，这会给证明带来巨大的麻烦。因此在验证这两个算法及其使用的大整数库时，我们进行了以下三层抽象。

第一层：非负大整数的数位数组表示。 用数组保存非负大整数的各个数位，底层函数直接操作数组指针和长度。这一层证明数组读写、复制和移位等操作符合要求，并建立多字算术的数值与进位关系。规约既说明结果数组表示的数值，也约束访问范围和所需的内存。

mp_limb_t 是保存大整数各位的无符号机器字类型；本验证实现使用 32 位的 unsigned int，基数为 B = 2³²。谓词 mpd_store_Z(B, p, v, n) 将数组与数值联系起来：从地址 p 开始的 n 个 limb，按低位在前的顺序编码非负整数 v。

mpn_* 函数直接操作这些数组。以 mpn_add 为例，结果数组保存低位，返回值保存最高位的进位。它的后置条件中有以下关系：

val_r_out + __return * Z::pow(UINT_MOD, an) == val_a + val_b

UINT_MOD 就是基数 B，an 是结果数组的长度。因此，数组表示的整数加上返回的进位，必须等于两个输入整数之和。规约还通过 mpd_store_Z 描述输入和输出的数组内存。

unsigned int
mpn_add(unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn)
/*@ non_alias
 With val_a val_b
 Require
   an >= bn && an >= 0 && bn >= 0 &&
   mpd_store_Z(UINT_MOD, ap, val_a, an) *
   mpd_store_Z(UINT_MOD, bp, val_b, bn) *
   UIntArray::undef_full(rp, an)
 Ensure
   exists val_r_out,
   (val_r_out + __return * Z::pow(UINT_MOD, an) == val_a + val_b) &&
   mpd_store_Z(UINT_MOD, ap, val_a, an) *
   mpd_store_Z(UINT_MOD, bp, val_b, bn) *
   mpd_store_Z(UINT_MOD, rp, val_r_out, an)
*/

第二层：带符号大整数的封装表示。 这一层将数位数组、正负号、有效长度和容量封装成一个大整数对象，证明内存分配、扩容和表示调整正确，并将对象上的运算与数学整数运算对应起来。例如，乘法接口保证结果对象表示的整数等于两个输入整数之积。上层调用这个接口时，只需使用整数层面的规约，无需再次展开数组和进位实现。

__mpz_struct 包含三个字段：指向 limb 数组的指针 _mp_d、记录数组容量的 _mp_alloc，以及用绝对值记录有效长度、用符号记录正负的 _mp_size。谓词 store_Z(x, n) 将这些字段、有效数据和剩余容量一起封装，表示地址 x 处的对象保存整数 n。

mpz_* 接口用这个谓词描述整数运算。例如，mpz_add 在三个对象互不重叠时的规约是：

void mpz_add(mpz_ptr r, mpz_srcptr a, mpz_srcptr b)
/*@ nonalias
  With n m l
  Require
    store_Z(a, n) * store_Z(b, m) * store_Z(r, l)
  Ensure
    store_Z(a, n) * store_Z(b, m) * store_Z(r, n + m)
*/

调用前，a、b、r 分别保存 n、m、l；调用后，输入不变，r 保存 n + m。调用者不用跟踪扩容、符号处理或逐位进位，这些工作由 mpz_add 的实现及其证明负责。

第三层：消元算法。 傅里叶消元和高斯消元复用上述大整数规约，证明系数计算和数据结构更新满足各自的算法要求。傅里叶消元在报告不可满足时，原约束集确实无解；正常返回消元结果时，输出约束由原约束蕴含，且待消变量的系数为零。高斯消元则保证，求解成功时，输出向量满足规约中描述的方程组。

例如，傅里叶消元组合两条约束时有以下调用（省略验证标注）：

mpz_mul(tmp, m1, r1 + i);
mpz_addmul(tmp, m2, r2 + i);

第一行计算第一个系数乘积，第二行再加上第二个系数乘积。使用这两个接口的规约，就能证明 tmp 保存了新约束所需的线性组合，无需重新证明底层乘法。高斯消元则用 mpz_array(aug, n * (n + 1), l) 将存储增广矩阵的大整数数组与整数列表 l 对应起来，再证明矩阵变换。

这样，大整数库只需针对自己的接口完成验证，两种消元算法就能共同使用这些结论。这个项目共验证了 83 个函数：两个消元程序调用的 61 个 mini-gmp 函数、8 个傅里叶消元函数和 14 个高斯消元函数。

验证规模

复杂算法与数据结构：证明具体实现满足算法要求

QCP 团队还在专家指导和审核下，通过 AI 自动执行或人机协作，完成了 233 个 C 程序实例的规约编写和验证，包括 86 个算法、数据结构与工程实例，以及 147 个 Codeforces 竞赛题实例。它们涉及排序、贪心、动态规划、图算法、数论和计算几何；Codeforces 题目评分覆盖 800–2800，其中 26 个不低于 2000。

例如，我们证明了基于二叉堆的优先队列的功能正确性，包括元素的插入、取出和优先级更新。Dijkstra 最短路算法和 Prim 最小生成树算法的相应实现使用了这些优先队列，因此在验证这两个算法时，我们复用了队列操作的正确性结论，在此基础上证明最短路径和最小生成树的性质，无需重复证明堆内部的元素交换和顺序调整。这样，同一数据结构的验证结果就可以用于多个算法的证明。

QCP 团队将这些实例的问题描述、C 代码、经专家审核的规约、标注和证明整理为 PV-BENCH。我们希望研究者能从中复用数据表示、规约设计和证明组织的经验，并以共同的任务评测规约生成、标注补全和证明构造方法，逐步提高 AI 独立完成程序验证的能力。

什么时候需要形式化验证？

是否需要形式化验证，首先取决于能否明确说出程序应当满足什么要求。对于有明确安全性和功能正确性标准的代码，可以考虑在开发过程中引入形式化验证。 测试可以帮助发现错误，形式化验证则进一步检查实现是否对所有满足前置条件的输入都遵守这些要求。

从有明确正确性要求的功能代码入手

后端服务、算法实现和承担具体业务功能的代码，通常都有可以明确描述的要求：哪些操作需要授权，数据更新应当保持哪些约束，计算结果必须满足什么关系。这些要求可以写成规约，并通过证明检查实现是否遵守规约。

形式化验证可以系统性地检查并保障这类代码的安全性与功能正确性。在安全要求被完整表达、设计满足这些要求、实现符合设计，并且运行环境满足约定的前提下，程序应当能够提供相应的安全保证。验证的作用，就是把这些条件和保证之间的关系明确建立起来。

没有明确判定标准的要求，不必强行形式化

对于主要承担展示、交互和组件连接的前端、UI 或 Glue Code，为整段代码构造形式化证明意义不大。界面是否美观、交互是否符合用户习惯，往往需要设计评审和实际使用来判断。如果其中包含权限控制、输入校验或数据处理等具有明确正确性要求的逻辑，这些部分仍然值得考虑验证。

同样，高频交易算法“能否盈利”取决于市场行为等外部因素，不能仅凭程序实现正确就得到保证。但它是否遵守给定的交易规则、是否正确计算订单和执行风险限制，可以成为形式化验证的目标。需要区分的是程序能够保证的行为，以及依赖外部环境才能实现的效果。

需求变化和环境复杂，不应成为放弃验证的理由

在以人工构造证明为主的工作方式下，一种保守的取舍是避开需求频繁变动的业务原型：需求一变，规约和证明就要一起维护。对于涉及硬件时序、操作系统中断或并发总线交互的代码，还需要把外部系统的行为纳入证明，例如中断可能何时发生、哪些数据可能被其他执行单元修改。这就是建立环境模型，也会带来较大的前期投入。

然而，这些恰恰是值得用 AI 改善的工作。需求变化时，AI 可以协助更新规约、定位受影响的证明，并在重新检查后修复它们。对于与硬件和操作系统交互的程序，AI 可以辅助整理接口假设、构造环境模型和补充证明；人需要确认这些模型是否准确描述了实际环境。

变化带来的是证明维护难度，复杂交互场景带来的是建模难度。我们希望借助 AI 降低这两类工作的成本，既让证明能够随程序修改而更新，也让复杂运行环境中的交互行为更容易被准确描述并纳入验证。 这仍然要求把环境假设写清楚，并用合适的验证工具检查；没有建模的行为不会因为使用了 AI 就自动得到保证。

目前 QCP 支持 C 程序验证，QCP 团队还计划逐步推出 C++、Java、Python 等语言的验证工具。你可以从入门教程出发，复现随附的 C 程序示例；也可以使用随附的 AI 工作流，尝试验证自己项目中的算法函数。

程序验证的未来

AI 已经能够参与编程，接下来的问题是：它能否在交付代码的同时，给出代码满足需求的证明？如果自动验证能力足够成熟，附带规约和形式化证明的程序，有望成为 AI 编程的日常交付结果。 工程师仍然通过讨论需求和关键设计来指导开发，AI 则负责把这些约定落实为实现和证明。

• 规划阶段：把需求变成可以检查的规约。 工程师像现在使用 plan mode 一样，与 AI 讨论要实现的功能，以及核心部分采用什么实现方式。AI 据此起草规约和关键证明步骤；人审核输入条件、输出保证和相关定义，确认它们准确表达了需求。
• 编码阶段：一起完成程序和证明。 AI 编写实现、补齐标注与详细证明，并调用验证工具检查。未通过时，继续修改代码或证明；若需要改变规约，则交回人确认。后续修改程序时，也重新检查证明，确认新的实现仍满足约定。

如果 AI 能够稳定地完成这些工作，工程师仍然可以像今天一样，通过讨论需求、确认方案和提出修改来推进开发。AI 交付的每一版代码都会附带与之对应的规约和证明，由验证工具检查它是否满足约定。形式化验证也就有望融入日常编程：代码不断迭代，证明随之更新，工程师则集中判断需求是否准确、设计是否合适。