长期以来，由于成本高昂且适用范围有限，Jane Street 对形式化方法持怀疑态度。然而，随着 AI 智能体编程的兴起，这一立场发生了根本转变。AI 生成的代码需要更严格的验证，而形式化方法不仅能减轻人工审查的负担，还能为 AI 智能体提供更强大的反馈。因此，该公司正在组建一个新团队，旨在将形式化方法与其在编程语言上的优势相结合，使其成为软件开发中一个普及且实用的工具。
过去：成本过高的工具
过去 25 年，Jane Street 一直认为形式化方法不值得投入。尽管他们是类型系统（一种轻量级的形式化方法）的坚定支持者并从中获益良多，但全面的形式化方法被认为成本过高。
- 高昂的成本： 一个典型的例子是 seL4 微内核项目，它花费了 25 人年的精力才验证了 8,700 行 C 代码。
- 不切实际的投入： 平均每行代码需要大约 23 行证明，以及半个人天的工作量来验证。
- 结论： 对于大多数软件，包括 Jane Street 的关键系统，这种投入产出比都是不合理的。
现在：AI 编程带来的转变
智能体编程 (Agentic coding) 的出现彻底改变了原有的成本效益分析，使 Jane Street 从怀疑转向兴奋。
这种转变主要源于两个方面：
- 成本降低： AI 模型极大地帮助了证明的构建，使得更多人能够高效地使用形式化方法工具。工具的易用性提升，使得重新评估其价值成为必要。
- 收益提升： 与此同时，形式化方法带来的好处也变得前所未有地重要。
形式化方法的新价值
在 AI 编程时代，形式化方法的收益体现在两个关键领域：
缓解验证瓶颈： AI 擅长生成代码，但代码质量往往参差不齐，充满了错误和不符合规范的实现。这导致人工审查成为一个巨大的瓶颈。形式化方法可以 自动化部分验证工作，让代码审查过程更高效。
为智能体提供反馈： AI 智能体依靠反馈来解决复杂问题和提升代码质量。测试是一种反馈，但其覆盖范围有限。形式化方法则能提供 更强大的反馈，例如类型系统带来的“全局保证”。
我们之所以对全面的形式化方法感到兴奋，很大原因在于我们看到了类型在与智能体一同编程时的巨大价值。
这种由类型系统提供的 普遍性保证 (universal guarantees) 能够彻底消除某些类型的错误（如数据竞争或跨站脚本攻击），这是单纯的测试难以做到的。
为什么在 Jane Street 推进？
Jane Street 认为自身在两个方面具有独特优势，适合在内部推动这项工作，而不是完全依赖外部工具或初创公司。
我们有两个优势：对我们所使用语言的深度控制，以及一个为此做好准备的程序员社区。
对语言的深度控制： 公司可以修改其核心编程语言，使其更好地与证明技术集成。这包括改进类型系统、增加所有权和可变性等约束，甚至将证明技术直接内置于语言中。
乐于接受新技术的用户： 与许多地方不同，Jane Street 的程序员社区渴望并积极要求更强大的类型系统功能。他们拥有合适的背景知识和追求高质量软件的内在动力，为尝试和推广新技术提供了理想的环境。