Jane Street Reverses 25 Years of Skepticism, Builds Formal Methods Team

For a quarter of a century, Jane Street's position on formal methods was simple: not interested. In a new post on the trading firm's blog, that position has changed. "I've been telling people for the last 25 years that Jane Street as an organization was just not interested in formal methods," the author writes. "I'm not saying that anymore."

Why the skepticism was reasonable

The post is careful to say the old stance was not obviously wrong. Jane Street leans heavily on tools that improve code quality, and type systems are themselves a lightweight form of formal methods that the firm has benefited from enormously. But full verification carried costs that rarely made sense outside special cases such as hardware synthesis. The canonical example is seL4, a formally verified microkernel and a genuine achievement: verifying 8,700 lines of C took about 25 person-years, with each line requiring roughly 23 lines of proof and half a person-day of effort.

Such a trade-off can be worth it for a security-critical microkernel, but not for most software — not even, the firm felt, its own most critical systems. Then agentic coding arrived.

What agentic coding changed

The cost side moved first: models cannot construct arbitrarily hard proofs alone, the author notes, but they automate much of the drudgery and put these tools in far more hands, changing the old arithmetic.

The benefit side moved too. Models are good at hitting a stated goal but worse at keeping a codebase healthy, and the result tends toward slop: overly complicated, full of odd bugs and corner cases, often violating invariants the rest of the code depends on. That makes the verification bottleneck costlier than ever, and proofs are a strong form of the feedback agents thrive on, in RL training and day-to-day coding alike.

Tests remain valuable — Jane Street points to property-based testing and fuzzing — but cannot cover the whole state space. Type systems give universal guarantees instead: a system that rules out data races removes all of them, and types that make cross-site scripting impossible do so categorically. Escape hatches such as Obj.magic exist, but can be tracked and banned.

Why build it in-house

Jane Street argues it is unusually well placed for this work. It controls OxCaml, its own variant of OCaml, which lets it reshape the language for proof-oriented techniques: modular specifications inside the type system, type-level constraints on ownership and mutability, proof methods built into the language. Its users want such features — the post notes they complain that promised type-system features arrive too slowly, while the hard part in most programming-language research is finding anyone to use new ideas in real work.

The team plans near-term improvements with immediate impact alongside longer-term goals, and will keep engaging with tools such as Lean, Dafny, Rocq, Agda and Iris. Jane Street is hiring in London and New York.