Formal Methods and the Future of Programming

Jane Street, a major financial firm, has reversed its long-standing skepticism of formal methods in software development, primarily due to the emergence of agentic coding (AI-assisted programming). While formal methods were previously considered too costly for most applications, AI agents reduce those costs while simultaneously increasing the need for verification, as AI-generated code tends to be unreliable and requires extensive review before release. The company now plans to build a team focused on making formal methods as widely useful as sophisticated type systems currently are in their development process.