tl;dr: Jane Street, long skeptical of formal methods due to their high cost (e.g., seL4 required 25 person-years to verify 8,700 lines of C), is now building a team to pursue them because agentic coding has shifted the cost/benefit calculus. LLMs lower the barrier to writing proofs, while simultaneously increasing the need for verification of AI-generated code and benefiting from the strong feedback signals formal methods provide. Jane Street believes its control over OxCaml and its receptive user base position it well to make formal methods as pervasive as type systems.