Formal Methods and the Future of Programming (blog.janestreet.com) AI

Jane Street’s Yaron Minsky argues that while the firm previously found full formal methods too costly compared with benefits, recent advances in agentic coding are making the tradeoff more favorable—both by increasing the need to verify messy, invariant-breaking agent output and by using formal methods as a powerful feedback mechanism alongside testing and type systems. He says the company is now building a team focused on formal methods, leveraging its control over the language (including OxCaml) and a user base that can support near-term improvements and longer-term proof-oriented directions, with hiring planned in London and New York.