十亿美元估值，AI数学公司开始验证代码

Brian Burns 在 X 上发了条推文：做 AI 数学的公司，凭什么从顶级风投拿十亿美元级别估值？数学很酷，但怎么赚钱？

他的答案是：自动形式化技术。这套技术原本是让 AI 把自然语言描述的数学定理，翻译成 Lean 这类数学证明助手能检查的形式语言。验证代码也是同样逻辑：把程序行为和规格翻译成形式化语言，交给机器证明它们一致。

AI 写出代码的速度，已经超过人类能审查的速度。网络安全形势吃紧，未来所有生产软件可能都要求通过形式化验证。这个市场有多大？整个软件行业。

Harmonic 已经入场。它今天宣布，从 C 和 Verilog 开始，用 AI 验证代码。原话是：“We're bringing Aristotle to code.” 把亚里士多德带到代码里。

Harmonic 给这句话配了一段视频。

C 语言是通用编程语言，Verilog 是硬件描述语言。一个是软件的地基，一个是芯片的地基。Harmonic 刚起步就把两个都占了，步子挺大。

形式化验证和测试不一样：测试在有限输入里找 bug，形式化验证用数学证明程序在所有情况下符合规格。以前多用在芯片设计、航空航天这类不能出错的地方。Harmonic 想把它变成 AI 写代码流水线里的一道自动质检。

推文评论区里，反应不一。有人说：“第一天就上 Verilog，是个炫技。” 还有人愿意为此付费：“我的 agent 写的东西一半能跑但总感觉哪里不对劲，我乐意花钱让工具在我发现之前抓住它。”

也有人泼冷水。一位网友贴出一张检测截图，图中显示 79% 的内容由 AI 生成，配文是：“你可以写脚本自己检测，AI 还没那么好。”

数学公司手里的证明能力，从象牙塔走进软件供应链。接下来要看的是，它能不能追上 AI 写代码的速度。