Jane Street 转向：因 AI 编程代理，形式验证将变得关键

shuchaobi · x · 2026-08-29

Jane Street 技术主管 Yaron Minsky 撰文回顾了公司 25 年来对形式验证方法的保守态度。过去认为其成本极高（如 seL4 内核验证成本），仅适用于高安全规格场景。

但 AI 编程代理的出现改变了这一视角。随着开发瓶颈从“实现”转向“规范与验证”，形式化语言（如 Lean）的重要性将大幅提升。Jane Street 现已组建团队，试图让形式验证像现在的类型系统一样普及，以确保 AI 生成代码的正确性。