Harmonic 发布 Aristotle：AI 定理证明器公开，可形式化验证 C 与 Verilog
xennygrimmato_ · x · 2026-10-28
Vlad Tenev 旗下的 Harmonic 宣布其 AI 定理证明器 Aristotle 正式公开可用，主打「让 AI 写的代码可被证明正确」。
- 能力：对 SystemVerilog/SVA 断言做形式化验证、证明 C 程序的内存安全；无需手写 spec，用自然语言描述应成立的性质即可，或由它自动提议关键属性。
- 流程：读取代码逐条构造证明（底层建模在 Lean 中），每个性质返回 proved / refuted / open 三种结论之一，并给出证明所依赖的假设，可接入每次 commit。
- 演示：现场复现 OpenSSL Heartbleed——对 1.0.1f 的 heartbleed.c，它能反驳两条安全性质（3 字节请求导致越界读 65,535 字节），并证明 1.0.1g 加入的两处长度检查使性质成立。
- 目标场景：网络安全、固件（出货后难打补丁）、流片前的芯片 RTL 验证——过去需要多年专家工作和高预算的形式化验证被自动化。
所属事件:Harmonic 公开 Aristotle：AI 形式化验证 C 与 Verilog(2 条相关)→
「编程与Agent」频道最新
- 观点：LLM 循环纠错的价值被低估了 — burny_tech · 2026-10-28
- 硅谷一年写 70 篇 Agent Infra 研究，国内基金几乎无人跟进 — FinanceYF5 · 2026-10-28
- 网友 vibe coding 出 Factorio×SimCity 混合城建游戏，手机也能玩 — AndyMasley · 2026-10-28
- Nitro 用形式化验证把 SQL 编译成 Rust，ETL 快 10 倍省 3 倍 — kuza55 · 2026-10-28
- 开发者自建 Grok 机器人连接器，用 Find My 定位苹果设备 — Baconbrix · 2026-10-28
- 调试 AI 编码 Agent 出错时，究竟需要哪些会话证据？ — Additional-Ladder-24 · 2026-10-28