Jane Street Blog - Formal methods and the future of programming

Formal methods and the future of programming

Jun 07, 2026 |

8 min read

Share on Facebook

Share on Twitter

Share on LinkedIn

By: Yaron Minsky

I’ve been telling people for the last 25 years that Jane Street as an organization was<br>just not interested in formal methods.

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<br>believers in the power of tools to help us write better and more reliable code. And type<br>systems are a kind of lightweight formal method that we’ve gotten an enormous amount of<br>benefit from. So you might expect us to have been big believers in more full-on formal<br>methods.

But outside of some special cases (notably, hardware synthesis), our sense has been that<br>formal methods were just not worth the costs for us. And those costs are really high!<br>seL4 is a great example of this. It’s a formally verified<br>microkernel, and a profound achievement. But, boy was it expensive to<br>do! It took 25<br>person-years of effort to verify 8,700 lines of C, and each line of code required<br>something like 23 lines of proof and a half a person-day to verify.

Our hope is to make formal methods as pervasively useful of a tool<br>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<br>stakes are high and the specifications are fairly clear. But it just doesn’t make sense<br>for most software, and to us it didn’t feel like it made sense for even our most critical<br>software.

But the emergence of agentic coding has changed our perspective, and we’ve gone from being<br>skeptical to being excited about the possibilities. And as a result, we’re now building<br>a team to focus on formal methods . Our hope is to make formal methods as pervasively<br>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<br>agents can on their own construct arbitrarily challenging proofs.1 But<br>models are enormously helpful, and broaden the set of people who can use these tools<br>productively. With formal methods being easier to use than ever, it’s worth reconsidering<br>the old cost/benefit calculus.

But things haven’t changed only on the cost side. The benefits seem bigger now too. There<br>are really two reasons for this:

The verification bottleneck is more important than ever . Models are increasingly good<br>at writing useful code. But there’s a big gap between the code that models generate, and<br>code that you’d want to actually release. To some degree, this is an artifact of how the<br>models are trained. They’re surprisingly good at achieving the goal you set in front of<br>them, but they don’t do a great job of maintaining and even improving the quality of the<br>codebase as they do so. Agentic code is getting better, but is still tends towards slop:<br>overly complicated, full of weird bugs and corner cases, often not following essential<br>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<br>is up to snuff. And formal methods could be a way of relieving some of that verification<br>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<br>using RL, and when you’re using agents to code. And formal methods are another powerful<br>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<br>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<br>valuable as well, and can be made even better by leaning into property-based<br>tests and<br>fuzzing. And lord<br>knows we’ve spent a lot of time building out testing<br>infrastructure.

But tests aren’t enough! There are inherent limits in the power of tests to cover the<br>state space that your program might explore. One of the things we’ve seen in our own<br>programming in OxCaml is that agents benefit a ton from universal<br>guarantees, the ∀ you get out of type systems. If your type system has a way of<br>preventing data races, it lets you<br>get rid of all2 data races. If you set up your types to make cross-site scripting<br>vulnerabilities impossible, then you can really get rid of those entirely, in a way that<br>mere testing has trouble doing.

Indeed, a lot of why we’re excited about full-on formal methods is that we see how<br>valuable types are when programming with agents, both for easing the verification<br>bottleneck and providing agents with better feedback, and that makes us excited to see how<br>much more uplift could be available by leveraging more powerful proof techniques.

We...