I’ve been telling people for the last 25 years that Jane Street as an organization was just not interested in formal methods.在过去的25年里，我一直告诉人们，Jane Street作为一个组织，对形式化方法并不感兴趣。

I’m not saying that anymore.我不再这么说了。

It’s not exactly that I think we were wrong all those years. To be clear, we’re strong believers in the power of tools to help us write better and more reliable code. And type systems are a kind of lightweight formal method that we’ve gotten an enormous amount of benefit from. So you might expect us to have been big believers in more full-on formal methods.我并不是说我们过去那些年都错了。明确地说，我们坚信工具能帮助我们编写更好、更可靠的代码。类型系统是一种轻量级的形式化方法，我们从中获益良多。所以你可能以为我们会大力支持更全面的形式化方法。

But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It’s a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.但除了一些特殊情况（特别是硬件综合），我们一直觉得形式化方法对我们来说不值得付出那些成本。而且那些成本真的很高！seL4就是一个很好的例子。它是一个经过形式化验证的微内核，是一项了不起的成就。但是，做这件事的成本太高了！验证8700行C代码花费了25人年的努力，每行代码需要大约23行证明和半人天来验证。

Our hope is to make formal methods as pervasively useful of a tool for building software as sophisticated type systems are for us today. 我们希望让形式化方法成为构建软件时普遍有用的工具，就像今天复杂的类型系统对我们一样。

That kind of approach could be worth it for a security-critical microkernel, where the stakes are high and the specifications are fairly clear. But it just doesn’t make sense for most software, and to us it didn’t feel like it made sense for even our most critical software.这种方法对于安全关键的微内核可能是值得的，因为风险高且规格相当清晰。但对于大多数软件来说，这根本不合理，而且对我们来说，即使是我们最关键的软件，似乎也不合理。

But the emergence of agentic coding has changed our perspective, and we’ve gone from being skeptical to being excited about the possibilities. And as a result, we’re now building a team to focus on formal methods. Our hope is to make formal methods as pervasively useful of a tool for building software as sophisticated type systems are for us today.但智能体编码的出现改变了我们的看法，我们从怀疑变成了对可能性感到兴奋。因此，我们现在正在组建一个专注于形式化方法的团队。我们希望让形式化方法成为构建软件时普遍有用的工具，就像今天复杂的类型系统对我们一样。

Why the change of heart?为什么会有这样的转变？

Agentic coding upsets the formal-methods apple-cart in a few ways.智能体编程在几个方面颠覆了形式化方法的传统格局。

For one thing, it dramatically changes the cost of using formal methods. It’s not that agents can on their own construct arbitrarily challenging proofs.¹ But models are enormously helpful, and broaden the set of people who can use these tools productively. With formal methods being easier to use than ever, it’s worth reconsidering the old cost/benefit calculus.首先，它极大地改变了使用形式化方法的成本。这并不是说智能体可以自行构建任意复杂的证明。但模型非常有帮助，并且扩大了能够高效使用这些工具的人群。随着形式化方法比以往任何时候都更容易使用，重新审视旧的成本/收益权衡是值得的。

But things haven’t changed only on the cost side. The benefits seem bigger now too. There are really two reasons for this:但情况不仅在成本方面发生了变化。现在收益似乎也更大了。这实际上有两个原因：

The verification bottleneck is more important than ever. Models are increasingly good at writing useful code. But there’s a big gap between the code that models generate, and code that you’d want to actually release. To some degree, this is an artifact of how the models are trained. They’re surprisingly good at achieving the goal you set in front of them, but they don’t do a great job of maintaining and even improving the quality of the codebase as they do so. Agentic code is getting better, but is still tends towards slop: overly complicated, full of weird bugs and corner cases, often not following essential invariants of the codebase that it’s a part of.验证瓶颈比以往任何时候都更加重要。模型在编写有用代码方面越来越出色。但模型生成的代码与你实际想要发布的代码之间存在巨大差距。在某种程度上，这是模型训练方式的结果。它们在实现你设定的目标方面出奇地好，但在维护甚至提高代码库质量方面却做得不够好。智能体代码正在改进，但仍然倾向于杂乱：过于复杂，充满奇怪的错误和边界情况，通常不遵循其所处代码库的基本不变量。

As a result, people need to spend a lot of time verifying that the code produced by agents is up to snuff. And formal methods could be a way of relieving some of that verification burden, and making the process of review a lot more efficient.因此，人们需要花费大量时间来验证智能体生成的代码是否合格。而形式化方法可以减轻部分验证负担，使审查过程更加高效。

Separately, agents thrive on feedback. This is true both when you’re training agents using RL, and when you’re using agents to code. And formal methods are another powerful form of feedback that can increase the agents’ ability to solve hard problems.另外，智能体依赖反馈。无论是使用强化学习训练智能体，还是让智能体编写代码，都是如此。而形式化方法是另一种强大的反馈形式，可以提高智能体解决难题的能力。

A lot of why we're excited about full-on formal methods is that we see how valuable types are when programming with agents. 我们之所以对完整的形式化方法感到兴奋，很大程度上是因为我们看到了类型在使用智能体编程时的价值。

Not that formal methods are the only way of getting feedback. Tests are incredibly valuable as well, and can be made even better by leaning into property-based tests and fuzzing. And lord knows we’ve spent a lot of time building out testing infrastructure.这并不是说形式化方法是获取反馈的唯一途径。测试也非常有价值，并且通过基于属性的测试和模糊测试可以使其变得更好。天知道我们在构建测试基础设施上花了多少时间。

But tests aren’t enough! There are inherent limits in the power of tests to cover the state space that your program might explore. One of the things we’ve seen in our own programming in OxCaml is that agents benefit a ton from universal guarantees, the ∀ you get out of type systems. If your type system has a way of preventing data races, it lets you get rid of all² data races. If you set up your types to make cross-site scripting vulnerabilities impossible, then you can really get rid of those entirely, in a way that mere testing has trouble doing.但测试还不够！测试在覆盖程序可能探索的状态空间方面存在固有的局限性。我们在OxCaml的编程中看到，智能体从通用保证（即类型系统提供的∀）中受益匪浅。如果你的类型系统能够防止数据竞争，它就能让你消除所有数据竞争。如果你设置类型使得跨站脚本攻击不可能发生，那么你就能真正彻底消除它们，这是单纯测试难以做到的。

Indeed, a lot of why we’re excited about full-on formal methods is that we see how valuable types are when programming with agents, both for easing the verification bottleneck and providing agents with better feedback, and that makes us excited to see how much more uplift could be available by leveraging more powerful proof techniques.事实上，我们之所以对完整的形式化方法感到兴奋，很大程度上是因为我们看到了类型在使用智能体编程时的价值，既能缓解验证瓶颈，又能为智能体提供更好的反馈，这让我们期待通过利用更强大的证明技术可以获得更大的提升。

We have two things going for us: deep control of the language we're using, and a community of programmers who are ready for this. 我们有两个优势：对我们所使用的语言的深度控制，以及一群准备好迎接这一挑战的程序员社区。

Why do it here?为什么在这里做？

One question this raises is: why is Jane Street well positioned to work on this problem? The whole world is thinking about what agents mean for the future of programming, and there are endless startups looking for ways of mixing formal methods and agents. Why is this something we’d work on internally? And why should formal methods experts in the outside world be excited to join our efforts here?这引发了一个问题：为什么Jane Street适合解决这个问题？全世界都在思考智能体对编程未来的意义，并且有无数的初创公司在寻找将形式化方法和智能体结合的方法。为什么我们要在内部做这件事？为什么外部的形式化方法专家应该兴奋地加入我们的努力？

For one thing, we have deep control of the language we’re using, and that lets us adjust that language to make it a better home for proof-oriented techniques. There are lots of potential directions to go here: from integrating modular specifications of properties into the type system, to adding type-level constraints around things like ownership and mutability to make certain kinds of proofs easier, to building proof techniques directly into the language.首先，我们对自己使用的语言有深入的控制，这使我们能够调整语言，使其更适合面向证明的技术。这里有很多潜在的方向：从将模块化的属性规范集成到类型系统中，到添加关于所有权和可变性等事物的类型级约束以使某些类型的证明更容易，再到将证明技术直接构建到语言中。

We also have a community of programmers who are ready for this, or at least more ready than any serious programming community I’ve encountered. For most people who work on programming languages, the easy part is coming up with new and better ideas about how to make programming better. The hard part is convincing anyone to actually use those ideas for real work.我们还有一个准备好迎接这一切的程序员社区，至少比我遇到过的任何严肃编程社区都更准备好。对于大多数从事编程语言工作的人来说，容易的部分是提出关于如何让编程变得更好的新想法。困难的部分是说服任何人真正将这些想法用于实际工作。

At Jane Street, things are different! We routinely have users angry at us because the new, weird type-system features we promised them aren’t coming fast enough. We have a lot of people with the right background to leverage these techniques, and a lot of baked in interest in getting things right and building high-quality software.在简街，情况不同！我们经常有用户因为承诺给他们的新的、奇怪的类型系统功能来得不够快而生气。我们有很多具备正确背景的人来利用这些技术，并且对把事情做对和构建高质量软件有着浓厚的兴趣。

We think that user base will gives us the freedom to try a mixture of approaches; there are some near-term improvements we think we can make which will have pretty immediate impact, and some ambitious, longer-term visions for where we can get in a few years. Having an engaged and excited user base makes both of these approaches possible, and lets us learn from the first, while we build towards the second.我们认为这样的用户群将给我们自由去尝试多种方法；有一些我们认为可以做出的短期改进将产生立竿见影的效果，还有一些雄心勃勃的长期愿景，关于几年内我们能达到的目标。拥有一个投入且兴奋的用户群使这两种方法都成为可能，让我们在构建第二种方法的同时从第一种方法中学习。

None of this is to say that we’re going to ignore work in the outside world. We’re excited and inspired by the work in a variety of other PL communities, built around tools like Lean, Dafny, Rocq, Agda, Iris, and too many more to mention. And we’re excited to look for ways of integrating OxCaml with some of these tools, to take advantage of the great infrastructure that’s already out there. But we also think there are some unique advantages that can only be realized by engaging with the language and the proof techniques at the same time.这并不是说我们将忽视外部世界的工作。我们对各种其他编程语言社区的工作感到兴奋和启发，这些社区围绕Lean、Dafny、Rocq、Agda、Iris等工具构建，还有太多无法一一列举。我们也很兴奋地寻找将OxCaml与其中一些工具集成的方法，以利用已经存在的优秀基础设施。但我们认为，只有同时处理语言和证明技术，才能实现一些独特的优势。

Join us!加入我们！

If this sounds interesting to you, consider applying! We’re looking for people in both London and New York. We’re in the early stages of interviewing people for these spots and building a team, and there’s an enormous amount of work ahead of us, and we’d love you to be a part of it.如果这听起来让你感兴趣，考虑申请吧！我们在伦敦和纽约都在招人。我们正处于为这些职位面试人员和组建团队的早期阶段，面前有大量的工作，我们很乐意你成为其中的一部分。

Footnotes脚注