正文

形式化验证很可能将在“反脆弱互联网”中发挥日益重要的作用。

我在 25 年春季曾亲自用 FV（Lean4）做过研究。当时它很难用，领先模型（Deepseek/4o）也处理不好它。但有几件事已经改变：

(1) 模型已经非常擅长 FV 语言。Lean4 现在是 AI 驱动数学突破事实上的实现方式，同样的技能也可迁移到代码。

(2) 端到端自动化更多了。在 @theoremlabs 与 @AnthropicAI 的合作中，现有的模糊测试会被自动转化为规约，而 Claude 会直接在编译后的 RISC-V 二进制文件上（用 Rocq）证明它们。数周内覆盖了 123 个开源库中的 239 个入口点。

(3) 近期的安全事件让“可验证代码”更受关注。FV 终于得到了其应得的资金和关注，而不再是一个（历史上较为边缘的）学术领域。

因此，这是代码中 FV 的一个令人兴奋的时期，尤其是对于像 @theoremlabs 这样致力于可验证代码的公司。但 FV 并非万能药，并不是任何经过验证的东西都“不可被黑”。有 3 点注意事项：

(1) FV 往往是追溯性的且不完整——其中很大一部分是在事后证明现有代码的属性，而且只覆盖测试能到达的路径，并不覆盖整个库或其他代码调用它的方式。

(2) FV 使用简化的沙盒——证明假定了简单的环境（例如单线程、静态链接、RISC-V），而这与实际在生产环境运行的代码之间仍有差距。

(3) 你必须恰当地定义属性——“安全”“无害”或“正确”等概念必须以数学方式明确下来，例如通过测试套件，而不能停留在高层次。当你说某样东西“安全”时，你真正表达的是：在范围内的任何输入下都不会发生坏事。