实测 Harmonic Aristotle 验证 Verilog：证明能过但产物遭质疑

10 月 29 日，研究者 thomasahle 在一系列帖子中分享了试用 Harmonic 数学定理证明模型及其形式化验证系统 Aristotle 验证硬件设计的全过程，对象是一个约 200 行的简单 Verilog 浮点除法文件（FPDivide.v / fpdiv，后确认为 IEEE-754 FP32 单精度，用户最初说的 FP64 系笔误）。结果喜忧参半：Aristotle 交出了形式化证明，仿真还额外发现缺陷，但 thomasahle 随后公开质疑证明产物的可信度与工程体验。

已确认

• Aristotle 成功证明了该电路的两项约定性质：确认端口为 32 位单精度，以及「商寄存器 bit 23 置位」「正常输入下除法结果按向零舍入逐位正确」等属性。
• 在形式化验证之外，仿真环节又揪出 5 类浮点 bug。
• Agent 具备多轮澄清提问设计：如验证时主动指出组合 always 块未在所有控制路径上赋值，并向用户追问澄清，获 thomasahle 好评。

尚未确认

• 证明的可信度：thomasahle 指出生成的文件里并不包含实际的证明，也没有从 Verilog 转译到 Lean 的版本，外界无法用 Lean 自行验证其正确性；他还称系统「号称已证明」的部分，用 Claude 花 $63 就能复现验证，暗示这部分工作未必需要 Harmonic 的系统。
• 卡顿与排队问题的根因（任务调度、算力限制还是产品策略）未获 Harmonic 方面解释，thomasahle 仅得知一次只能跑一个项目。

为什么重要

这是对「LLM + 形式化方法」验证真实硬件设计的一次端到端实测。能力层面 Aristotle 交出合格答卷（正确性性质成立、还能借仿真发现缺陷），但 thomasahle 的质疑点中了要害：形式化验证的价值恰恰在于可独立复核的证明产物，若交付物不含可验证的证明与 Verilog→Lean 转译，结论就难以被第三方检验。叠加工程体验短板——读 200 行代码耗时 27 分钟且停留在「working」状态、无任何进度或思考提示、排队等了 10 分钟、并发任务受限（系统提示「进行中或等待开始的任务过多，请等一个完成或停止一个再试」）——对希望在日常芯片验证流程中引入此类 Agent 的开发者而言，可验证性、吞吐与可观测性都是必须先解决的问题。

2026-10-29 ~ 2026-10-29 · 6 条相关

• 实测 Harmonic 数学 Agent:为形式化验证 Verilog 主动追问澄清问题 — thomasahle · 2026-10-29
• Harmonic Agent 限制并发任务数:排队过长遭用户吐槽 — thomasahle · 2026-10-29
• 用户吐槽 Harmonic 的 Aristotle：200 行 Verilog 卡死无进度提示 — thomasahle · 2026-10-29
• 【源头】Harmonic 数学模型形式化证明 200 行 Verilog 浮点除法正确性 — thomasahle · 2026-10-29
• 【源头】Aristotle 形式化验证 fpdiv 电路，仿真再揪出 5 类浮点 bug — thomasahle · 2026-10-29
• 【源头】质疑 Harmonic 电路证明：产物不含真实证明，$63 就能用 Claude 复现验证 — thomasahle · 2026-10-29