Jane Street 对形式化方法与编程未来的看法

Jane Street 正在转变其在形式化方法上的组织立场，从怀疑转向积极投资，通过建立一个专门的团队，将这些技术集成到其软件开发生命周期中。这一转变是由智能体编程（agentic coding）的兴起所驱动的，它在降低生成形式化证明成本的同时，也增加了对 AI 生成代码进行严格验证的必要性。

智能体编程作为形式化方法的催化剂

智能体编程从解决实现成本和日益增长的可靠性需求两个方面，从根本上改变了形式化方法的成本效益分析。

降低证明成本

历史上，形式化方法的价格极其昂贵。例如，seL4 微内核需要投入 25 人年才能验证 8,700 行 C 代码，每行代码大约需要 23 行证明。现在的 AI 智能体通过自动化将证明思路编码为满足证明系统格式的枯燥工作，降低了这一门槛，从而扩大了能够高效使用这些工具的开发者群体。

解决 AI 验证瓶颈

虽然 AI 模型编写功能性代码的能力日益增强，但它们经常产生“slop”——即过于复杂、包含微妙漏洞或违反核心代码库不变性的代码。这造成了验证瓶颈，即人类必须花费大量时间确保 AI 生成的代码达到生产就绪状态。形式化方法通过提供测试无法提供的数学保证，提供了一种可扩展的方式来减轻这一负担。

增强智能体反馈循环

AI 智能体在精确的反馈中茁壮成长。虽然基于属性的测试（property-based testing）和模糊测试（fuzzing）很有价值，但它们无法覆盖程序的整个状态空间。形式化方法提供通用保证（使用 $\forall$ 量词），允许开发者完全消除整类漏洞——例如数据竞争（data races）或跨站脚本漏洞（cross-site scripting vulnerabilities）。这种严谨的反馈循环提高了智能体解决复杂问题的能力。

Jane Street 的战略实施

由于对工具链的控制以及内部文化，Jane Street 认为自己处于推进形式化方法的独特地位。

语言控制权与 OxCaml

通过对其所使用的语言（特别是 OxCaml）保持深度控制，Jane Street 可以修改语言以更好地支持面向证明的技术。潜在的方向包括：

• 将属性的模块化规范直接集成到类型系统中。
• 为所有权（ownership）和可变性（mutability）添加类型级约束。
• 将证明技术直接构建到语言语法中。

类型系统采用的文化

与许多挑战在于如何说服开发者采用新工具的组织不同，Jane Street 拥有一个积极要求更先进类型系统特性的程序员社区。这种内部需求使得该公司能够尝试即时的短期改进和宏大的长期愿景。

行业观点与反论点

围绕 Jane Street 举措的社区讨论突显了形式化方法应用中的几个关键张力。

映射问题与领域限制

一些批评者认为，形式化方法在代码实现确定性算法、且规范与领域之间的映射为 1:1 时最为有效。对于探索性工作或 UI 开发，存在“地图并非领土”的问题，使得形式化规范变得不太实用。

正如一位评论者所言：

"In theory, there is no difference between theory and practice. In practice..."

"Workarounds" 的风险

存在一种担忧，即极端的数学严谨性可能导致适得其反的行为。类似于一些 Rust 开发者使用“技巧”来绕过借用检查器（borrow checker），程序员可能会为了赶进度而寻找绕过形式化约束的方法，从而可能破坏安全保证。

现有证明助手（Proof Assistants）的角色

行业从业者已经注意到，在 Rocq (以前是 Coq) 和 Lean 4 等助手中，使用前沿模型完成证明的有效性。一些人建议，AI 完成“困难”证明义务的能力可能会使形式化方法的重点从“让机器更容易进行证明”转向“向人类展示清晰的证明”。

验证的局限性

尽管有形式化验证，漏洞仍然可能存在。评论者指出，即使是经过形式化验证的 seL4 微内核也遇到过漏洞，这表明形式化方法只是更广泛的加固策略中的一层，必须包含 ASAN、SAST 和 fuzzing。