For a quarter-century, Jane Street steered clear of heavyweight formal methods, convinced that the costs outweighed the benefits except in niche areas like hardware synthesis. The team points to seL4, the formally verified microkernel: verifying 8,700 lines of C took 25 person-years, producing 23 lines of proof per code line and half a person-day to check each. Despite their faith in strong type systems, they saw full formal verification as too slow and rigid for most of their trading infrastructure. Now, agentic coding—using AI models that write and refine code—has shifted that balance. Models cut into the expense of proof generation and lower the barrier for nonexperts. But ML-generated code still arrives messy: tangled logic, hidden bugs, violated invariants. That creates a “verification bottleneck.” Jane Street believes formal methods can automate much of the review work and feed precise, universal feedback back into the agents, speeding both correctness checks and agent training. Jane Street plans to build an internal formal-methods team. They already control OCaml, their primary language, and can extend it with proof-friendly features: modular property specs, ownership and mutability constraints at the type level, even embedded proof tactics. Their developer community is unusually receptive. Engineers here grumble when advanced type features lag behind requests, and they’ve built a culture that prizes code quality and rigorous reasoning. They don’t intend to reinvent tools like Lean, Dafny or Coq. Instead, they’ll integrate those ecosystems where it makes sense while pushing OCaml forward in tandem. The goal is a spectrum of improvements: quick wins in testing and property checks, and longer-term explorations of deep proof automation within the language. Jane Street is hiring in London and New York to tackle this, hoping to blend academic proof techniques with the realities of high-stakes trading software.