Harmonic 推出 Aristotle：自动形式化验证 C 与 Verilog 代码
satnam6502 · x · 2026-10-28
Harmonic 发布 Aristotle，一款对软件和硬件做形式化验证的 AI，首发支持 C 和 Verilog。定位是：AI 写的代码越来越多，没人审得动，Aristotle 负责「证明它是对的」。
工作流程：指向代码后，用自然语言描述应恒成立的性质（或让它自动提议关键性质），AI 逐步求证，最终给出证实/证伪/未决的判定并附每条证明的前提假设，可在每次 commit 上运行。演示中它能证伪 OpenSSL heartbleed.c，并证明 1.0.1g 修复版成立；代码在 Lean 中建模。
主打场景：网络安全、固件、流片前的 RTL/芯片设计验证——传统形式化验证需要专家团队数年与高额预算，Aristotle 想把它交给每个工程师。
所属事件:Harmonic 公开 Aristotle：AI 形式化验证 C 与 Verilog(2 条相关)→
「编程与Agent」频道最新
- 多模态 GraphRAG 处理飓风损毁评估:连缺失与矛盾证据也能建模 — JeremyCMorgan · 2026-10-28
- vibe coding 亲历:个人项目 20 小时工作量压缩到 2 小时 — gleech · 2026-10-28
- LangChain 开源 Slack 设计 Agent，揭秘如何编码审美对抗 AI 味 — BraceSproul · 2026-10-28
- 创业者：AI 写 95% 代码后，连 PR 审查也交给了 AI Agent — Yuchenj_UW · 2026-10-28
- 红杉联合 OpenAI 办扑克 AI 锦标赛:60 分钟从零造 bot,冠军奖金 10 万美元 — polynoamial · 2026-10-28
- Nyxis 开源：用 Lean 形式化证明保证 AI 写的后端不会越权泄露 — udmrzn · 2026-10-28