AI 推动形式化验证创业潮：&Truth 融资 7000 万美元

核心事实

据 WIRED 报道，一家名为 &Truth 的创业公司于周四公开亮相，已从投资者处融资 7000 万美元，目标是最终能验证任何编程语言。斯坦福研究者 Chuyue Sun 于今年 8 月加入该公司。她与同行在一篇近期论文中报告，其 AI 工具用不到半天、不到 500 美元完成了一项工程任务，而三名高水平专家手工完成同样工作耗时五个月。该研究还借助 AI 验证了通讯应用 Signal 中部分加密对话代码。

背景与影响

形式化验证指用数学方法证明软件按预期运行，过程漫长繁琐，企业过去很少为此付费。如今多家公司押注生成式 AI 能降低门槛：Harmonic 获 2.95 亿美元融资，称其数学导向的 AI 智能体 Aristotle 支持验证 C 语言软件与 Verilog 硬件设计；Anthropic 与 Theorem 上周联合宣布用 AI 协助发现开源软件中的缺陷，并为 Claude 推出验证插件。&Truth 首席科学官 Ilya Sergey 以桥梁建筑前先做数学计算作类比。据公司披露，波音飞机、亚马逊服务器及超过 25 亿台在用苹果设备中已包含部分经过形式化验证的软件。

限制与来源

该技术仍处原型阶段。报道指出，需求虽高，但客户愿付多少、偏好何种采用方式尚不清楚。形式化验证依赖对计算机与人如何与软件交互的假设，有专家怀疑其难以捕捉用户误操作与硬件故障引发的缺陷。Antithesis 的 Will Wilson 称形式化验证对其这样的数学爱好者是「陷阱」，过程是「一件苦差事」，并称只有稳健的穷尽测试才能证明保证成立。Vitalik Buterin 亦撰文称形式化验证并非万能药。本文信息来自 WIRED 报道，相关公司融资、产品能力与可用范围以官方当前信息为准。