AREX Feed Article
Robinhood CEO Vlad Tenev 联合创办的 Harmonic 宣布 Aristotle 扩展至软件与芯片设计验证，率先支持 C 与 Verilog
周二（10 月 27 日），由 Robinhood CEO Vlad Tenev 联合创办的 AI 初创公司 Harmonic 宣布，其 Aristotle 模型从数学证明扩展至软件与芯片设计验证：Aristotle 自当日起可以对以 C 语言编写的软件和以 Verilog（一种硬件描述语言）编写的芯片设计进行形式化验证，产品当天开放自助注册、按用量计费。，的原话是：“形式化验证历来缓慢、昂贵，而且基本只属于专家。Aristotle 要把它交到任何工程团队手里。”
最具体的落地证据来自客户。美国聚变实验室 DIII-D 表示，Aristotle 仅凭一篇研究论文和一段 254 词的提示词，在四小时内复现了其等离子体控制系统中的一个算法，验证了相应 C 代码的安全性，并生成逻辑等价的 Verilog 代码用于硬件加速。把这次发布放进“AI 检测软件缺陷的应用正受到更多审视”的背景下：就在几天前，AI 工具此前发现的关键 PHP 漏洞刚被公开披露并配上紧急补丁，引发全球争相修补。
官方口径的边界：C 的功能正确性，Verilog 的流片前验证
按的说法，支持 C 之后，Aristotle 可以对照指定要求验证软件，“包括功能正确性，以及不存在某些类别的未定义行为”；对 Verilog，它提供“覆盖控制路径属性（如活性 liveness 与安全性 safety）与数据路径数学属性的整体逻辑验证”。写得更直接：C 语言用户可以“证明它没有未定义行为”；Verilog 用户可以“在流片（tapeout，即设计交付制造）前证明你的 RTL（寄存器传输级）正确，包括活性”。Verilog 和 C 是目前仅有的两种支持语言，页面上“更多语言”一栏标着“即将推出”。
Harmonic 在 把动机说得很短：“AI 写代码的速度已经超过所有人的审查能力。我们在构建验证这些代码的 AI。从今天起，先支持 C 和 Verilog。”公告则引用 Harmonic 联合创始人兼 CEO Tudor Achim 的话：“这一扩展的意义不止于开发者如何构建软件。对依赖软硬件的业务来说，对关键系统做数学验证提供了一条新路，能在缺陷和漏洞变得代价高昂或构成灾难之前发现它们。”
不写规格书：说出“必须成立什么”，拿到机器检查的裁决
公告解释了它与测试、代码审查的区别：后两者“只检查一部分可能的行为”，而 Aristotle 用形式化验证“在给定系统内，对所有可能的输入，数学地证明指定属性是否成立”。
把流程拆成三步：工程师把 Aristotle 指向自己的代码，不需要先写规格书，用平实的英语描述“什么应该永远成立”，或者让 Aristotle 自己提议值得检验的属性；Aristotle 读取代码、逐步构造证明，如果推翻某条属性，会说明原因；最后返回裁决——已证明、已推翻，或无法判定（left open），并附上每条证明依赖的假设。产品页强调：“证明要么通过机器检查，要么不通过，所以没有置信度分数需要解读。”每份报告列出证明了什么、依据哪些假设、哪些没被覆盖。工程上的落点是持续集成：工程师审查属性、提交进代码库，之后每次提交都跑一遍 Aristotle，“让已被证明的保持被证明”。
供职于 Harmonic 的 Satnam Singh 在 举了一个横跨软硬件的例子：Aristotle 可以形式化验证 SystemVerilog 及其断言（SVA），也可以“证明一个 C 模型与其 SystemVerilog 实现等价”——也就是把软件模型和硬件设计对起来核对。他写道，“我们的 AI 定理证明器现已公开可用”。
DIII-D 与 Tensordyne：两份具名客户证言
DIII-D 国家聚变设施的 Mitchell Clark 在 的证言中说：“为聚变反应堆开发实时控制系统，需要在严格的安全要求与快速推进新诊断、新物理和控制算法之间求平衡。Aristotle 的形式化验证能力从根本上改变了我们应对这一挑战的方式。仅凭一篇研究论文和一段 254 词的提示词，Aristotle 在四小时内复现了我们等离子体控制系统中的一个算法，验证了 C 代码的安全性，并生成了逻辑等价的 Verilog 代码用于硬件加速。”路透社的报道把这件事概括为“重建了其反应堆控制软件的一部分”。这一说法目前来自 DIII-D 与 Harmonic 的单方陈述：引语刊于 Harmonic 官网，路透社亦予报道。
芯片设计一侧也有具名用户。Tensordyne 的 ASIC 验证工程师 Jonathan Ko 在同一页面说，形式化验证过去“意味着陡峭的学习曲线和手写属性”，而 Aristotle 让设计工程师在早期 RTL 编写阶段就得到即时反馈，让验证工程师“能对传统工具不敢想的状态空间做形式化验证”，还会把功能与微架构规格对照 RTL 做审计、标出歧义。Achim 在 证实这是与 Tensordyne 的联合工作。
公告背后的 PHP 危机：三支团队、两种大模型、一个 14 年的老漏洞
路透社在报道中写道，“研究人员最近利用该技术发现了 PHP 中的关键漏洞，引发全球争相修补”，但没有点名具体工具。补上了细节：10 月 21 日，维护 PHP 的 PHP 基金会披露两个“严重”漏洞并发布紧急补丁，编号 CVE-2026-109618 与 CVE-2026-109619，合称 php2shell；未打补丁的系统可被攻击者远程执行代码，基金会敦促网站立即安装补丁，否则暂时下线。
发现过程横跨三支团队，全都用上了 AI：AI 红队公司 Calif 受邀加入 OpenAI 的 Patch the Planet 计划后调查 PHP，于 8 月 1 日用 OpenAI 的 GPT-5.6 Sol 找到第一个问题；OpenAI 随后自行深挖，发现了漏洞的更多环节；Google 旗下的安全公司 Wiz 也在 8 月独立调查 PHP，于 8 月 19 日发现首个问题，用的是 Google 的 Gemini 4 Argon、GPT-5.6 Sol 加上自家的 Wiz Atlas。OpenAI 总裁 Greg Brockman 指出，这个漏洞在 PHP 里已经存在了 14 年，其受限版本 2024 年被发现但当时未被视为重大。OpenAI 称，是它把各方拉进了协同披露与修补的联盟，成员包括 Wiz、Calif、PHP 基金会、Cloudflare 及多个美国政府机构等。
后果是看得见的：安全公司 Palo Alto Networks 的初步分析识别出 2260 万个潜在受影响实例；全球大多数网页运行在 PHP 上，支撑着约 40% 网站的 WordPress 也不例外；Cloudflare 的 CTO Dane Knecht 称已观察到“早期攻击”；据路透社报道，荷兰和芬兰的部分政府机构为防范风险直接把网站下线，FBI 网络部门、美国国家安全局（NSA）、欧盟计算机应急响应团队和日本首相等相继发声敦促更新。Wiz 在公布研究的博客中写道：“受影响的互联网规模达 70%，php2shell 的影响再怎么估计都不为过。这标志着一个 AI 拐点——有漏洞的代码在那里放了十多年，AI 改变的是理解这些弱点、并把它们变成可用攻击的能力。”
一周前，Anthropic 用 Claude 证明了 123 个开源库
Harmonic 不是唯一在这条赛道上出成果的公司。10 月 21 日，Anthropic 与 Theorem 合作：用 Claude 为 Google OSS-Fuzz 计划（为合格开源项目提供持续模糊测试）中 123 个开源库的 239 个入口点证明了“任何小于 64 MB 的输入都不会导致崩溃”。这些证明作用在编译后的 RISC-V（一种处理器指令集架构）汇编代码上，总计约 1.8 亿行 Rocq（一种机器证明检查工具）证明代码，单个证明典型约 60 万行，对应二进制的中位长度为 18,000 条 RISC-V 指令。写证明的过程本身还找出数百个 bug，其中包括需要约 20 MB 的特定输入布局才触发的越界写——这类缺陷靠模糊测试很难碰到。
Anthropic 在文中解释了形式化验证过去为何昂贵：seL4 操作系统内核的实现花了两人年，而形式化验证花了 20 人年，因此这项技术此前基本只在真正任务关键的领域可行，比如空中客车的航电代码。它同时给自己的结果划了边界：这些证明并不意味着相关库不再含有任何 bug——需要信任的环节包括 RISC-V 与 Linux 进程的形式模型、被证明的定理陈述本身，以及 Rocq 证明检查器。Anthropic 称，据其所知，这是首个在汇编代码层面对生产软件做大规模 AI 形式化验证的努力，并预计“随着模型能力继续提升，形式化验证将成为安全软件开发的重要组成部分”。
从 IMO 金牌到 VERINA 96.8%：Aristotle 的来路和没回答的问题
Harmonic 对自己的定位是构建“数学超级智能”（mathematical superintelligence），一个以推理为核心、旨在减少幻觉与事实错误的 AI 系统——这是转述的公司口径。Aristotle 的能力轨迹也沿着数学到代码：Harmonic 称它是；2025 年 12 月，它在代码验证基准 VERINA（由 UC Berkeley 与 Meta 的研究者开发）的 189 道形式规格中证明 160 道正确、推翻 23 道，解决率 96.8%，远高于基准论文作者当时测试的通用大模型——直接作答 3.6%，加入迭代后 22.2%。它还能为不成立的规格找出反例，比如证明“取列表中出现次数第 k 多的整数”这道题的规格本身写错了。
资金面，；据路透社报道，本轮融资金额 1.2 亿美元，估值 14.5 亿美元，投资方包括 Nvidia 的风险投资部门、Sequoia 与 Ribbit Capital。
这次发布留下的问题同样具体。公布当天，从事 AI 韧性研究的 Nora Ammann 在 写道，希望“尽快看到更多细节（例如 C 用的是什么形式模型），以及这些证明能被独立复现”。至于 Verilog 和 C 之外的语言，Harmonic 的产品页目前只有“即将推出”一行字。