The outcome first: Jane Street is hiring a formal-methods team. The reason is what makes it a story.
On June 7, Yaron Minsky - the man who talked the firm into using OCaml back in 2002 - opened a post with a line you almost never read from a serious engineering shop. "I've been telling people for the last 25 years that Jane Street as an organization was just not interested in formal methods. I'm not saying that anymore." Then the receipt: they're building a dedicated team.
I pay attention to reversals more than launches. A launch tells you what a company hopes will work. A reversal tells you what changed its mind after years of betting the other way - and Minsky is specific about what changed. Agentic coding moved the numbers on both sides of a calculation the firm had run the same way for a quarter century.
The old math
You can't read the reversal without the price tag it overturns.
Formal methods means proving a program correct - not running it against test cases, but proving, mathematically, that it does what its spec says for every input. The standing reference for what that costs is seL4: a small operating-system core (a microkernel) and the first general-purpose OS kernel to earn a complete, machine-checked proof of functional correctness. A real achievement. Also an expensive one.
By the numbers - the cost that kept everyone out
- 8,700 lines of C in the kernel.
- ~200,000 lines of Isabelle proof script to verify them.
- ~23 lines of proof for every line of code.
- ~20 person-years for the proof, per the original paper (Klein et al., SOSP 2009) - roughly 9 of those years building reusable proof tooling, about 11 specific to seL4.
A note on that last figure, because it's the kind of thing this column exists to get right. Minsky's post rounds the cost to "25 person-years" and "half a person-day" per line. The primary paper's own number is the ~20 person-years above. I'm citing the paper, not the paraphrase. The exact figure doesn't change the verdict - either way, the answer for 25 years was the same: worth it for a security-critical microkernel with a clean spec, not worth it for normal software, and by Jane Street's own read, "not even for our most critical software."
Worth being precise about what they rejected. Not proof itself - Minsky calls type systems "a kind of lightweight formal method," and the firm has leaned on those hard for years. What they rejected was the cost of going further. At 23 lines of proof per line of code, the math wasn't close.
What moved the number
Minsky's case is that agentic coding cut the cost and raised the benefit at the same time. Both, not one.
Cost side: models are "enormously helpful" at writing proofs, and they "broaden the set of people who can use these tools productively." He doesn't oversell it - a footnote concedes that on a genuinely hard proof the model still needs a human to supply the strategy; it handles the drudgery, not the insight. But cheaper-to-attempt changes what's worth attempting, and that's the whole game when the old objection was cost.
Benefit side, and this is the part operators should sit with: the verification bottleneck. Minsky's description of agent-written code is not a vendor's: it "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." Agents are good at hitting the goal and bad at keeping the code clean while they do it. So humans now spend real time checking agent output, and that checking is the cost that keeps climbing as you ship more agent code. Formal methods are a way to make that check cheaper and more certain.
There's a second benefit: agents "thrive on feedback," in training and in coding both, and a proof obligation is about the most unambiguous feedback you can hand one.
The strongest point is the one about coverage. Tests sample what a program might do; they have, in Minsky's words, "inherent limits" on covering that space. A guarantee at the type or proof level covers all of it. His examples are concrete: a type system that forbids data races eliminates every data race; types that make cross-site scripting impossible eliminate that whole class of bug - not in the cases you tested, everywhere. That "everywhere" is what tests structurally can't buy you, and it's worth more the more code is being written by something that doesn't share your sense of which invariants matter.
Why it's Jane Street saying it
Read the fine print before you copy the homework.
Jane Street has two advantages most shops don't. It controls its own language - OxCaml, a modified OCaml - so it can bend the language toward proofs instead of fighting one it doesn't own. And it has programmers who actually want this: Minsky notes the firm regularly has users "angry" that promised type-system features aren't shipping fast enough. For most language designers the hard part is getting anyone to adopt the good idea. Jane Street's problem is the opposite, and that's rare.
Which is exactly why the transferable lesson is not "go adopt proofs." A firm with its own compiler and a bench of people who enjoy advanced type systems is close to the best case formal methods will ever get. Most companies have neither, and pretending otherwise is how a good finding becomes a bad mandate. For the record, this isn't an isolationist bet either - Minsky names Lean, Dafny, Rocq (formerly Coq), Agda, and Iris as work they're drawing on and want to integrate with.
What actually shipped
Here's where I keep myself honest. This is a reversal and a hiring plan. It is not a measured result.
Jane Street is "in the early stages" of interviewing, with open roles in London and New York. There's no before-and-after number - no "verification time fell X percent" - because the team is only now forming. Anyone waving this around as proof that formal methods plus agents work at scale is citing a job posting as an outcome. What's documented is the decision and the reasoning. That's it. That's also enough to matter.
Because the decision is the data point. A firm whose entire business is high-stakes software, which spent 25 years pricing formal methods as too expensive to bother with, now prices the cost of not verifying agent-written code high enough to staff a team against it. The line item that moved is the verification bottleneck - the distance between code that hits the goal and code you'd actually put into production. Formal methods are one answer to that, and a hard one to copy. The bottleneck is the part every operator who ships agent code already owns. Jane Street just put a headcount on it.
