Formal methods are techniques that mathematically prove software behaves exactly as specified; the firm's lead for OCaml, a functional programming language the firm uses heavily, says agentic coding — AI systems that generate and check code in iterative loops — has finally re…
Twenty-five person-years. Eight thousand seven hundred lines of C. Twenty-three lines of proof for every line of code. That's what it took to formally verify the seL4 microkernel in 2009, according to the Klein et al. paper at SOSP 2009. For most of the two decades since, the economics of formal verification, the discipline of mathematically proving software behaves exactly as its specification says, have stayed that brutal. Now a quant trading firm famous for its OCaml obsession is betting that agentic coding has finally changed the math.
On June 7, 2026, Yaron Minsky, who leads the OCaml group at Jane Street, published a blog post titled "Formal methods and the future of programming" announcing that the firm is building a dedicated formal methods team. The move reverses roughly 25 years of organizational skepticism. Minsky frames it explicitly as a reversal, not an evolution: Jane Street is, in his telling, doubling down on a class of techniques it had long treated as too expensive for ordinary software.
Minsky's argument for why the math has changed runs through two related mechanisms. First, agentic coding, in which AI agents generate and check code in iterative loops, lowers the human cost of constructing and verifying formal proofs. Second, those same agents benefit from formal feedback: a richer, more precise signal than unit tests or type errors, useful for reinforcement learning and for keeping agent-generated code inside the lines. "Agentic coding upsets the formal-methods apple-cart," Minsky writes, in phrasing the post leans on.
The historical anchor Minsky uses is seL4. Citing the Klein et al. SOSP 2009 paper, he restates the figures: about 25 person-years to verify roughly 8,700 lines of C, with approximately 23 lines of proof per line of code, and roughly half a person-day of effort per line. Those numbers have stayed famous precisely because they make the cost legible. The seL4 documentation site tracks the microkernel's continued status as the canonical formally verified kernel and an active research ecosystem, but the underlying point in Minsky's framing is that no one has seriously claimed that ratio has dropped to something an ordinary team could absorb.
Jane Street's structural advantage, in Minsky's telling, is its control of OCaml and its in-house dialect OxCaml, plus an internal programmer community that already demands and uses advanced type-system features. The argument is that new proof-oriented language features would have a real user base from day one, the same way incremental type-system work has for years. Concrete near-term directions Minsky names: modular property specifications integrated into the type system, type-level ownership and mutability constraints, and embedding proof techniques directly in the language. OxCaml and DrFCaml, Jane Street's data-race-free OCaml variant, are referenced as the bridge from "types" to "formal guarantees" that the team is building on.
The post is careful to position formal methods as complementary to, not replacing, the firm's existing testing infrastructure: expect tests, property-based testing, which Minsky cites from a 2024 ICSE paper by Harrison Goldstein and collaborators, and fuzzing. The implication is that agentic coding widens the population of people who can use formal methods productively, the way IDEs and type systems once widened who could write robust software, rather than replacing proof engineers with autonomous theorem provers.
The honest open question sits underneath the announcement. Formal verification has historically been defensible in security-critical niches, microkernels, cryptographic implementations, hardware synthesis, where the cost of a bug is high enough to justify a 25-person-year bill. The Jane Street case is interesting precisely because the firm sits outside that niche: a quant trading shop, where the work is complex, performance-sensitive, and reviewed to the bone, but not formally verified end to end. If agentic coding has genuinely re-priced formal methods, the question is whether the new math extends to ordinary critical software at ordinary software companies, or only to the security-critical enclaves that were already paying the bill.
There is a second limit worth naming. The June 7 post is one senior voice at one firm. Minsky does not name team size, budget, leadership hires, or a product timeline, and the reversal is directional rather than operational. There is no public Jane Street hiring post or external job listing that independently corroborates the new team, and the seL4 cost figures that anchor the argument are taken from Minsky's restatement of the Klein et al. paper, not from an independent read of the PDF body. The "agentic coding" category is also a moving target, and the forward-looking framing here is dated to the post itself: by the time a reader reaches the end, anything in Minsky's argument about models' current capabilities is already the claim of a single author on a single day.
What to watch, then, is concrete. Whether Jane Street's new team publishes language features, proof tooling, or both. Whether other firms that already use formal methods, in hardware verification, security, or safety-critical software, agree the economics have shifted, or push back. And whether the ratio that anchored seL4 in 2009, 23 lines of proof per line of code, ever moves enough to matter for a team that is not a security lab.