有趣。实际上，AI 将同时增加形式化方法的需求和供给。你更需要它们，但你也拥有了让它们更便宜的工具。

https://t.co/t4QFZueL9c

形式化方法与编程的未来

来源：https://blog.janestreet.com/formal-methods-at-jane-street-index/ 过去 25 年里，我一直在告诉别人，Jane Street 作为一家机构，对形式化方法没有兴趣。

我现在不再这么说了。

倒不是说我认为那些年我们都错了。明确一点，我们坚信工具能帮助我们编写更好、更可靠的代码。而类型系统是一种轻量级的形式化方法，我们从中获益匪浅。所以你可能认为我们会是更全面的形式化方法的坚定支持者。

但除了一些特殊情况（尤其是硬件综合），我们一直觉得形式化方法对我们来说并不划算。而成本确实很高。

seL4 就是一个很好的例子。它是一个经过形式化验证的微内核，也是一项了不起的成就。但是，它的代价非常高昂！(https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf)验证 8700 行 C 代码花费了 25 人年的努力，而每行代码大约需要 23 行证明和半个工作日来验证。

我们希望让形式化方法成为构建软件的通用工具，就像今天复杂的类型系统对我们一样。

这种方法对于安全关键的微内核来说可能是值得的，因为风险很高，规格也相当明确。但对于大多数软件来说，这并不合理，对我们而言，即使是最高关键的软件，它似乎也不合理。

但智能体编程的出现改变了我们的看法，我们从怀疑转向了对其可能性的兴奋。因此，我们现在正在组建一个专注于形式化方法的团队。我们希望让形式化方法成为构建软件的通用工具，就像今天复杂的类型系统对我们一样有用。

为什么态度转变了？

智能体编程在几个方面颠覆了形式化方法的现状。

首先，它极大地改变了使用形式化方法的成本。这并不是说智能体可以独立构建任意具有挑战性的证明。1 (https://blog.janestreet.com/formal-methods-at-jane-street-index/#fn:not-all-proofs)但模型非常有帮助，并且扩展了能够有效使用这些工具的人群。随着形式化方法变得比以往任何时候都更容易使用，重新审视旧的成本/收益计算是值得的。

但情况不仅在成本方面发生了变化。现在看来收益也更大。这主要有两个原因：

验证瓶颈比以往任何时候都更为重要。模型在编写有用的代码方面越来越出色。但模型生成的代码与你实际想要发布的代码之间存在巨大差距。在某种程度上，这是模型训练方式的产物。它们在实现你设定的目标方面出奇地好，但在这个过程中，它们并不擅长维护甚至提高代码库的质量。智能体代码正在变得更好，但仍然倾向于杂乱无序：过于复杂，充满奇怪的错误和边界情况，通常不遵循其所处代码库的基本不变量。

因此，人们需要花费大量时间来验证智能体生成的代码是否达标。而形式化方法可以减轻部分验证负担，使审查过程更加高效。

另外，智能体依赖反馈。无论你是在使用强化学习训练智能体，还是使用智能体进行编程，这都是事实。而形式化方法是另一种强大的反馈形式，可以提高智能体解决困难问题的能力。

我们之所以对全面的形式化方法感到兴奋，很大程度上是因为我们看到了在智能体编程中类型是多么有价值。

当然，形式化方法并不是获取反馈的唯一途径。测试也非常有价值，并且可以通过利用基于属性的测试 (https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf) 和模糊测试 (https://blog.janestreet.com/getting-from-tested-to-battle-tested/) 来做得更好。天知道我们在构建测试基础设施 (https://blog.janestreet.com/the-joy-of-expect-tests/) 上花了多少时间。

但光有测试是不够的！测试覆盖程序可能探索的状态空间的能力存在固有局限性。我们在 OxCaml (http://oxcaml.org/) 的自身编程中看到的一件事是，智能体从全局保证中获益巨大，即从类型系统中得到的 ∀。如果你的类型系统有办法防止数据竞争 (https://richarde.dev/papers/2025/drfcaml/drfcaml.pdf)，它就能让你消除所有2 (https://blog.janestreet.com/formal-methods-at-jane-street-index/#fn:all) 数据竞争。如果你将类型设置成使得跨站脚本攻击变得不可能，那么你真的可以完全消除这些攻击，这是单纯测试难以做到的。

事实上，我们之所以对全面的形式化方法感到兴奋，很大程度上是因为我们看到了类型在智能体编程中是多么有价值，既能缓解验证瓶颈，又能为智能体提供更好的反馈，这让我们很兴奋地想看看通过利用更强大的证明技术可以带来多大的提升。

我们有两个优势：对我们使用的语言有深入的控制，以及一群为此做好准备的程序员。

为什么在这里做？

这引出一个问题：为什么 Jane Street 适合解决这个问题？全世界都在思考智能体对编程未来的意义，有无数初创公司在寻找将形式化方法与智能体结合的方法。为什么我们要内部研究这个？为什么外部的形式化方法专家会乐于加入我们的努力？

首先，我们对我们使用的语言有深入的控制，这让我们能够调整该语言，使其更适合基于证明的技术。这里有很多可能的方向：从将属性的模块化规范集成到类型系统中，到在类型层面添加关于所有权和可变性的约束以使某些类型的证明更容易，再到直接将证明技术构建到语言中。

我们还有一群为此做好准备的程序员，或者至少比我遇到过的任何严肃编程社区都更准备好。对于大多数从事编程语言工作的人来说，容易的部分是想出新的更好的想法来改善编程。困难的部分是说服人们实际在工作中使用这些想法。

在 Jane Street，情况不同！我们经常有用户对我们生气，因为我们承诺给他们的新的、奇怪的类型系统功能发布得不够快。我们有很多人具备利用这些技术的合适背景，并且对把事情做对、构建高质量软件有着根深蒂固的兴趣。

我们认为，这个用户群将赋予我们尝试混合方法的自由；有一些近期改进我们认为可以做出，将会产生立竿见影的效果，还有一些雄心勃勃的长期愿景，关于几年内我们可以达到的目标。拥有一个积极投入且兴奋的用户群使得这两种方法都成为可能，并让我们在构建长期目标的同时，从第一种方法中学习。

这并不意味着我们将忽视外部世界的工作。我们对各种其他编程语言社区的工作感到兴奋和启发，这些社区围绕诸如 Lean (https://lean-lang.org/)、Dafny (https://dafny.org/)、Rocq (https://rocq-prover.org/)、Agda (https://hackage.haskell.org/package/Agda)、Iris (https://iris-project.org/) 等工具以及太多无法一一提及的工具而建立。我们也很高兴寻找将 OxCaml 与其中一些工具集成的方法，以利用已经存在的基础设施。但我们也认为，只有同时处理语言和证明技术，才能实现一些独特的优势。

加入我们！

如果你对此感兴趣，请考虑申请！我们在伦敦 (https://www.janestreet.com/join-jane-street/position/8588405002/) 和纽约 (https://www.janestreet.com/join-jane-street/position/8585303002/) 都在招聘。我们正处于为这些职位面试和组建团队的早期阶段，前面有大量的工作要做，我们很乐意你成为其中的一员。

Yaron Minsky 于 2002 年加入 Jane Street，并声称拥有说服公司开始使用 OCaml 的可疑荣誉。