QuickProof 让 C 代码规格用代码本身编写，AI 代理自动生成形式化证明

几十年来，要证明软件正确，有两个问题让大多数开发者望而却步：规约必须用 Lean 或 Rocq（原 Coq）这类证明助手的语言来写，而且证明很长，往往比代码长好几倍。第二个问题正在消失。现在 AI agent 会写形式化证明，证明检查器会验证每一步，所以错误的证明无法通过。 第一个问题依然存在，而 agent 让它变得更重要。证明检查器保证的是所陈述的定理被证明了，而不是它就是你想要的那个定理。找不到证明的 agent 可能会弱化陈述或添加假设，而如果你读不懂陈述，你就无法分辨。 QuickProof 为 C 解决了第一个问题。它让你用代码本身的语言来写规约：一个小 C 程序，调用你的库，很像一个测试。QuickProof 把它变成定理，AI agent 证明它，Rocq 检查证明。agent 写的任何东西都不需要被信任。 本文展示如何用 QuickProof 陈述并证明生产 C 代码的性质。同样的流程能发现 bug，即使是在已经验证过的库里。 让我们拿经典的压缩往返性质来说：解压必须还原被压缩的内容。在 QuickProof 中，规约是一个 C 程序： int main(void) { uint8_t data[4096], packed[8192], unpacked[4096]; size_t n = nondet_size(); // any length ... qp_assume(n <= sizeof data); // ... up to 4 KiB nondet_bytes(data, n); // any contents size_t m = compress(data, n, packed); size_t k = decompress(packed, m, unpacked); // decompressing gives back the original data qp_assert(k == n && memcmp(unpacked, data, n) == 0); return 0; 它读起来像一个基于性质的测试，带有三类特殊函数： 测试检查它碰巧尝试的输入。证明覆盖规约允许的每一个输入：在这里，是每一个不超过 4 KiB 的字节串。 下面是 QuickProof 对这个规约所做的： 首先，qp assemble 把规约和你的库变成 Rocq 证明助手中的一个定理：每个 qp_assert 对每个允许的输入都成立，并且代码没有未定义行为（详见下文）。定理陈述在任何证明工作开始之前就已固定。 然后 AI agent 在 Verified Software Toolchain（VST）中证明它，这是一个用于 C 的 Rocq 框架。它们编写 compress 和 decompress 的函数规约、它们的循环不变式和证明，并且只能修改证明文件。如果 decompress 在某个输入上丢了一个字节，证明就会卡住，agent 会去寻找那个输入：你会得到一个带复现用例的 bug，而不是一个定理。 最后，qp verify 从全新克隆重建证明并检查两件事：陈述未变，以及证明只使用标准公理。所以 agent 无法通过弱化陈述或假设待证内容来作弊。 翻译很简单，而这正是 QuickProof 可信的原因。我们使用 VST，一个用于推理 C 程序的 Rocq 框架，在 Princeton 开发了十多年，例如用于验证 OpenSSL 的 SHA-256。对于规约的 main，我们在 VST 中唯一陈述的是它没有未定义行为（特别是，它是内存安全的）。 我们向程序的环境恰好添加三个规约，每类特殊函数一个。正是它们把“性质成立”变成“没有未定义行为”。 所以定理陈述的是，无论 nondet_* 调用返回什么值，规约的每次通过其 qp_assume 的运行都满足其所有 qp_assert 并且没有未定义行为。这排除了内存错误（越界访问、释放后使用、双重释放、空指针解引用、读取未初始化内存）、除以零、错误移位和有符号溢出，在你的库中以及规约中都是如此。 我们选取了几十个流行的 C 项目并为它们编写规约。对于其中一些，我们让 AI 把文档中做出的承诺翻译成规约，然后我们自己审查这些规约。仅此而已就足够了：在尝试证明这些规约时，我们发现了 300 多个代码违反它们的 bug。 Theorem 和 Anthropic 最近验证了 Linux 内核的一个核心组件，并得出结论它“几乎完全正确”，除了少数次要的、在角落情况下无法利用的 bug。当我们验证同样的代码时，我们发现了一个存在了二十年、可被远程利用来关闭设备的缺陷。我们已将其报告为 CVE。 Redis 把小的哈希、列表和流存储在 listpack 中，这是一种带有自己格式规范的紧凑格式。格式规范定义了什么是有效的 listpack，而 Redis 承诺接受有效的 listpack。所以我们的规约说：每个按格式规范有效的 listpack 都通过 Redis 的深度验证并准确读回。 int main(void) { struct model m; // any listpack, written by the rules of the listpack specification unsigned char *lp = write_any_listpack(&m); qp_assume(lp != NULL); // Redis's deep validation accepts it ... qp_assert(lpValidateIntegrity(lp, lpBytes(lp), 1, NULL, NULL) == 1); // ... and reading it gives back every entry that was written unsigned char p = lpFirst(lp); for (size_t i = 0; i < m.n; i++) { qp_assert(entry_is(p, &m, i)); p = lpNext(lp, p); qp_assert(p == NULL); return 0; write_any_listpack 和 entry_is 来自格式规范的 C 模型，几百行代码，根据其表格编写：写入器使用 nondet_ 选择条目，并以格式规范允许的每一种方式编码它们。 在 Redis 8.10 上，这个规约的证明卡住了。在三种条目长度（16,383、2,097,151 和 268,435,455 字节）下，listpack 格式允许条目长度字段有两种编码。Redis 8.6 及之前写的是较长的那种。8.8 中的一个修复切换到了较短的那种，但同一个函数也被用于读取现有条目。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）