从 Vibecoding 到 Vericoding

半个工作日换一行正确的代码

seL4 是一个微内核——8700 行 C 代码。为了证明这 8700 行代码的功能正确性，研究团队花了 20 人年，写了 200000 行 Isabelle 证明脚本。每行实现代码对应 23 行证明。算下来，每行代码的正确性证明大约耗费半个工作日。

这个数字解释了一件事：为什么形式化验证在过去几十年难以走出高保障领域和研究社区。不是因为它没用——恰恰相反，seL4 大概是世界上最值得信赖的操作系统内核之一。最硬的约束首先是经济学：没有几个项目能承受每行代码半天的验证成本。航天、军事、医疗器械能用，你的 Web 应用不能。

有人会说，seL4 是 2009 年的数字，现在的工具链进步了很多。的确如此。但即使效率提高 10 倍，每行代码仍然需要接近一个小时的专家工时。对于一个十万行级别的项目，这仍然意味着数千个人天。对大多数项目而言，成本仍然没有下降到可以忽略的程度。

Vibecoding 的幻觉困境

2025 年以来，AI 代码生成的主流用法可以概括为 vibecoding：你用自然语言描述意图，模型生成代码，你看一眼觉得差不多就用了。这个工作流快得惊人，但有一个结构性缺陷——幻觉。

模型生成的代码看起来合理、语法正确、甚至能通过简单测试，但逻辑上可能是错的。一个排序函数可能在大多数输入上正常工作，但在边界条件下悄悄返回错误结果。一个并发锁的实现可能在低负载时完美运行，在高负载时产生死锁。这些错误的危险在于隐蔽性：代码的外观和行为都指向”正确”，直到它不正确为止。

一旦场景要求可靠性，幻觉就会成为决定性的约束，因为整个工作流依赖人类的判断力。你必须看懂代码才能判断它对不对。但如果你有能力逐行审查代码的正确性，你大概率也有能力自己写。这就是 vibecoding 的悖论：它对专家来说是提效工具，对非专家来说是信心陷阱——你以为你验证了代码，其实你只是觉得它看起来对。

这不是在否定 vibecoding 的价值。对于原型开发、探索性编程、一次性脚本，vibecoding 已经是生产力的飞跃。但对于需要正确性保证的场景，它的天花板卡在人类审查的带宽和可靠性上。人类审查代码会累、会走神、会被模式匹配欺骗。你不能把系统的可靠性建立在一个不可靠的验证环节上。

完美验证器：一个反直觉的洞察

2025 年 12 月 8 日，Martin Kleppmann 发了一篇文章，提出了一个反直觉的观察：在形式化验证领域，AI 的幻觉问题根本不重要。

他的原话是：“It doesn’t matter if they hallucinate nonsense, because the proof checker will reject any invalid proof.”

这句话的核心在于 “proof checker”——证明检查器。一个数学证明要么有效，要么无效，没有中间状态。不存在”看起来正确但其实错了”的证明，因为检查器会逐步验证每一个推导步骤。这和代码完全不同：代码可以在 99% 的输入上正确而在 1% 的输入上出错，但证明不行，任何一步推导错误都会导致整个证明被拒绝。

这意味着证明检查器是一个完美验证器——对给定形式系统中的证明对象，它的判断是确定性的，不依赖人类直觉。这里的“完美”只针对“证明步骤是否合法”，不针对“规约是否正确”。

有了完美验证器，AI 的工作模式发生了根本改变。模型不需要一次生成正确的证明——它可以生成 100 个候选证明，只要其中 1 个通过检查器，任务就完成了。幻觉？无所谓。99 个胡说八道的尝试加 1 个正确的证明，结果等价于 1 次完美的生成。

这是一个深刻的结构性差异。在 vibecoding 中，每一次生成都需要人类判断是否正确，错误的生成不是零成本而是负成本——它会误导你，让你以为代码是对的然后部署到生产环境。但在形式化验证中，错误生成的外部性显著更低：它不会像错误代码那样悄悄混入生产环境，而是被检查器直接拒绝。算力成本仍然存在，但失败模式更干净、可自动化处理。

用更精确的方式表述这个区别：vibecoding 的验证器（人类审查）是概率性的、有限带宽的、会疲劳的；形式化验证的验证器（证明检查器）是确定性的，可以低边际成本地重复运行，也不会像人类审查那样疲劳。前者的可靠性有硬上限，后者的瓶颈主要转移到了规约、搜索和工程组织上。

Leanstral：从理论到数据

如果这只是理论上的可能性，那它和过去二十年关于形式化验证的美好愿景没什么区别。但 2026 年 3 月 16 日，Mistral 发布了 Leanstral，把理论变成了具体的数字。

Leanstral 是一个专门用于 Lean 4 定理证明的语言模型，119B 参数，6.5B active（MoE 架构），Apache 2.0 开源。它在 FLTEval 基准上的表现值得逐项拆解。

绝对性能。 Leanstral 单次生成（pass@1）得分 21.9。对比：GLM5-744B 得分 16.6，Kimi-K2.5-1T 得分 20.1。一个推理时仅激活 6.5B 参数的专用模型，单次表现就超过了参数量大它一到两个数量级的通用模型。至少在 FLTEval 上，专用化的收益远超直觉中的“参数越大越强”。

并行采样的收益。 pass@2（生成 2 个候选取最好的）得分跳到 26.3。pass@16 达到 31.9。每多一次采样，分数都在稳定上涨——这正是完美验证器带来的结构性优势。在没有完美验证器的场景里，多次采样的价值递减很快，因为你还需要人来从多个候选中挑出最好的。但有了证明检查器，挑选过程是自动的，边际成本极低。

成本——最关键的维度。 Leanstral pass@1 的成本是 $18。Sonnet 4.6 得分 23.7，成本 $549。Opus 4.6 得分最高 39.6，成本 $1650。

这些数字之间的比值才是真正的故事：

• Leanstral pass@2 得分 26.3，超过 Sonnet，成本 $36——便宜 15 倍。
• Leanstral pass@16 得分 31.9，超过 Sonnet 8 分多，成本 $290——仍然比 Sonnet 便宜约 1.9 倍。
• Opus 单次成本 $1650，是 Leanstral 单次 $18 的 92 倍。

至少在这类有强验证器兜底的任务上，FLTEval 给出的信号是：强验证器会系统性地偏向“便宜、可多次采样”的模型。

这和通用代码生成的竞争格局完全不同。在缺少强验证器兜底的代码生成里，人们通常更愿意为更强的模型付费，因为单次生成的正确率更重要，或者至少”大概率对”。但在有完美验证器的场景里，你不需要模型聪明到一次就对——你需要它便宜到可以试很多次。验证的成本是固定的（运行一次检查器），生成的成本可以通过专用小模型压低到几乎可以忽略。

回头看 seL4 的数字：8700 行代码，20 人年，每行半个工作日。如果 Leanstral 级别的模型能自动生成并验证证明步骤，那个”半个工作日”的量级会发生什么变化？我无法给出确切数字——FLTEval 基准和工业级内核验证之间还有很大距离。但成本下降的方向和速度是明确的。

验证光谱：从完美到够用

到这里有一个合理的质疑：形式化验证很好，但现实中大部分代码不需要数学证明级别的正确性保证。一个电商网站的购物车逻辑需要在 Lean 4 里写证明吗？

不需要。但”完美验证器模式”的价值不限于形式化证明。验证器的强度是一个连续光谱，证明检查器只是光谱最强的一端。重要的是，光谱上的每个位置都适用同样的经济学逻辑：在验证器覆盖关键错误类型、且验证成本低于人工审查成本的前提下，验证越强、越自动化，生成质量的门槛通常就越低，并行采样也越值得。

2026 年 3 月 16 日，Peter Lavigne 写了一篇文章，提出应该用 property-based testing 加 mutation testing 来验证 AI 生成的代码。他的核心主张：“We should treat the output like compiled code.”——把 AI 的输出当作编译产物，而不是人类写的源码。

这个类比精确地击中了要害。你不会逐行阅读编译器生成的汇编来判断它对不对——你运行测试。同理，AI 生成的代码也不应该依赖人类逐行审查，你应该建立自动化的验证管道。

把验证手段排成光谱：

• 形式化证明（Lean, Isabelle, Coq）：完美验证器。证明通过后，正确性获得数学意义上的保证。幻觉影响：零。
• Property-based testing + mutation testing：不完美，但如果性质设计得当，能比普通单元测试更有效地暴露逻辑错误。Property-based testing 用随机生成的输入检验属性是否成立；mutation testing 通过故意修改代码来检查测试套件是否真的能捕获错误——本质上是在”测试你的测试”。幻觉影响：大幅降低。
• 强类型系统：Rust 的所有权系统在编译期排除整类内存安全问题。依赖类型（dependent types）能编码更多业务不变量。不如形式化证明强，但覆盖面广、成本极低。幻觉影响：部分消除。
• 传统单元测试：最弱的自动化验证。只覆盖你想到的 case。幻觉影响：有限降低。
• 人类审查：vibecoding 的现状。幻觉影响：取决于审查者的能力和精力。

光谱上的位置越高，“完美验证器模式”的效果越强。但即使在光谱中间，增强验证也能显著改变经济学。假设你用 property-based testing 能自动捕获 80% 的逻辑错误——这意味着人类只需要审查剩下的 20% 的潜在问题，工作量降了一个数量级。

这里的关键洞察是：提升代码可靠性的杠杆不在”让 AI 生成更好的代码”，而在”让验证更强更自动化”。 前者受限于模型能力的缓慢增长和收益递减（从 90% 正确到 95% 正确很难，到 99% 更难），后者可以通过工程手段实现跳跃式的改善。

具体来说：支付结算规则、协议状态机、加密库、并发内核组件，更适合往形式化证明或模型检查走；而后台 CRUD、报表生成、胶水代码，更现实的路径是 property-based testing 加 mutation testing。选择验证手段的依据不是”越强越好”，而是”错误的代价有多大”。

直面盲点：specification 从哪来？

我需要面对这篇文章论点中最薄弱的地方。

形式化验证需要一个正确的 specification——你要证明代码符合某个规约。但规约本身从哪来？谁来保证规约是对的？

如果 AI 生成了代码，也生成了规约，然后证明代码符合规约——你得到了一个自洽但可能完全偏离真实需求的系统。证明检查器只能告诉你”代码确实做了规约说的事情”，但不能告诉你”规约说的是你真正想要的事情”。

更麻烦的是，很多真实世界 bug 根本不是”实现错了”，而是”需求本身后来变了”或者”规约一开始就漏了边界条件”。形式化验证不能替你发现遗漏——它只能把”实现是否符合规约”这件事做扎实。

这不是一个能被技术绕过的问题。Specification 的正确性最终依赖人类对需求的理解，而这和 vibecoding 面临的挑战在根源上是同构的：人类必须有能力判断某个东西是否符合自己的意图。

但区别在于审查的对象。在 vibecoding 中，你需要审查整个实现——每一行代码的具体逻辑。在 vericoding 中，人工审查的重点会更多地转向 specification 和抽象边界，而不是逐行检查全部实现。审查”这个排序函数应该返回一个有序数组，且输出是输入的排列”比审查快速排序的具体分区实现容易几个数量级。

Specification 是否正确？这个问题永远需要人类回答。但 vericoding 把问题从”这几千行实现对不对”压缩到了”这几行规约对不对”。审查面积有机会显著缩小。

这不是消除了人类判断的必要性，而是把人类判断放在了它最擅长的位置——高层语义，而不是底层实现。

Vericoding 这个词

“Vericoding”这个术语来自 2025 年 9 月的一篇论文（arXiv: 2509.22908）。论文构建了一个跨越 Lean、Dafny 和 Verus 三种验证语言的基准，包含超过 12000 个任务。

这篇论文的意义不只在技术上。它做了一件文化上的事情：给这种”AI 生成 + 形式化验证”的工作流起了一个名字。

Vibecoding 之所以能迅速传播，部分原因是它给一种工作流起了个足够顺口的名字。Vericoding 做了对称的事情，但指向相反的方向：不是”凭感觉写”，而是”可验证地写”。有了名字，一种实践才能被讨论、被推广、被作为一种选择放在 vibecoding 旁边供人比较。

现实不会从 vibecoding 一夜跳到形式化证明。但投入的主方向应该从”继续赌模型少犯错”转向”建设更强的自动化验证”。

文化鸿沟

技术信号已经足够强了。Lean 4 是成熟的证明语言，Leanstral 是 Apache 2.0 开源的，证明检查器在笔记本上就能运行。至少在特定任务和特定成本结构下，已经出现了经济可行性的迹象。

但大多数开发者不会在明天开始写 Lean 证明。障碍不是技术，是文化。

形式化验证出身于数学和理论计算机科学。它的语言——dependent type、tactics、inductive propositions——对大多数写 TypeScript 和 Python 的开发者来说属于另一个知识体系。这不是智力差距，是接触面的差距。大多数 CS 教育不教形式化验证，大多数公司的工程文化不接受形式化验证，大多数工具链不集成形式化验证。

Kleppmann 预测 AI 会让形式化验证走向主流。我认为方向对了，但文化惯性可能比他预期的更大。技术可以在一年内成熟（Leanstral 的发布证明了这一点），更现实的阻力是：大多数团队没有写规约的习惯，没有把验证接进 CI，也没有预算为“机器可证明的正确性”买单。这类组织层面的变化通常比技术变化慢得多。

不过有一个理由保持乐观：Leanstral 是开源的，Lean 4 的工具链在积极发展，社区在增长。如果有人基于这些构建出一个足够好用的 IDE 集成——让开发者像运行 pytest 一样运行形式化证明——文化鸿沟可能比预期缩小得更快。

历史上，每一次验证工具的易用性跨越都带来了采纳的跳跃。类型检查从可选到默认花了大约十年（TypeScript 的崛起是一个缩影）。Linting 从”有人用”到”不用就是不专业”花了更短的时间。形式化验证的易用性跳跃还没有发生，但 AI 可能正是那个催化剂——不是因为 AI 让开发者学会了写证明，而是因为 AI 代替开发者写证明，开发者只需要写 specification。

最终推动变革的不会是论文或博客文章（包括这篇），而是一个足够低摩擦的工具。如果有一天”给这段代码写一个正确性证明”真的接近”跑一次 lint”的成本，vericoding 很可能会像类型检查一样自然渗透进日常开发。

回到经济学

这篇文章的核心论点用一句话概括：AI 代码生成的真正杠杆不在生成端，在验证端。

Vibecoding 沿着生成端发力——更聪明的模型、更大的上下文窗口、更精准的指令理解。这条路有收益递减的问题：模型从 90% 正确到 95% 正确是一个进步，但你仍然需要人类来找出那 5% 的错误。人类审查的成本不会因为错误变少而线性下降——审查整个代码库的认知负担基本是固定的。

Vericoding 沿着验证端发力。如果你有一个足够强的验证器，生成质量的重要性会显著下降——错的被自动拒绝，对的被自动接受。如果你有一个次完美验证器（比如 property-based testing），生成质量也没那么重要——大部分错误被自动捕获，人类只需要处理漏网之鱼。

在这两条路的交汇处，经济学发生了根本性变化。

seL4 的 20 人年和 200000 行证明脚本不再是形式化验证的唯一参照系。Leanstral 用 $18 跑出 21.9 的 FLTEval 成绩，$290 跑出 31.9。这些数字距离工业级应用还有距离——FLTEval 基准题和真实项目的复杂度不在一个量级——但成本下降的曲线是指数级的，而且小模型、并行采样、验证器这三个变量各自都在独立进步。

形式化验证的经济学正在从”只有航天和军工用得起”向”初创公司也能考虑”移动。速度有多快？我不确定。但方向没有悬念。

等形式化验证变得足够便宜的那天，回头看 vibecoding 的年代，大概会像我们现在回头看没有类型检查的年代——不是不能用，而是：为什么要冒这个险？