Harmonic 推出 Aristotle：用形式化方法自动验证 AI 生成的代码
wellecks · x · 2026-10-28
数学 AI 公司 Harmonic 宣布将旗下定理证明系统 Aristotle 从数学证明扩展到代码与硬件验证：用户用自然语言描述代码必须满足的性质，Aristotle 自动完成形式化证明，每个性质返回 proved / refuted / open 三种结论及假设依据，可在每次提交时运行。
要点：
- 今日起支持 C 语言和 Verilog，瞄准「AI 写代码的速度已超过人工审查能力」这一痛点。
- 用户无需是形式化验证工程师：可以纯英文描述性质，也可让系统自动提议最重要的性质。
- DIII-D 国家聚变设施案例：仅凭一篇论文和 254 词的 prompt，Aristotle 4 小时复现其等离子体控制算法、验证了 C 代码安全性，并生成逻辑等价的 Verilog 用于硬件加速。
- 芯片公司 Tensordyne 反馈：传统形式化工具门槛高，Aristotle 近乎「fire-and-forget」，还能对照 RTL 审计功能规格、标记歧义。
所属事件:Harmonic 公开 AI 定理证明器 Aristotle，可验证代码与硬件(4 条相关)→
「编程与Agent」频道最新
- 单卡 3090 跑 DeepSeek-V4.1-Flash 量化版，41 tok/s 且 90% 对齐官方 API — musicurgy · 2026-10-28
- Resend 发布面向 Agent 的 Inboxes 产品，开发者 3 个月高产复盘 — philnash · 2026-10-28
- 设计团队自述:AI 通宵探索品牌方案,人类只做决策 — thesephist · 2026-10-28
- 「追逐 Karpathy 之峰」：AI 研究员自述过度依赖 AI 掉进 Slop 悬崖 — anshulkundaje · 2026-10-28
- USearch v3 发布候选版亮相，作者晒出开源库被55万星项目依赖的成绩单 — viglovikov · 2026-10-28
- Agent 时代来临：工程学科边界正在消融 — yunta_tsai · 2026-10-28