Harmonic launches Aristotle, an AI theorem prover that formally verifies C and Verilog code
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 验证——过去需要多年专家工作和高预算的形式化验证被自动化。
Related event: Harmonic Unveils Aristotle for Formal Verification of C and Verilog(2 posts)→
More from coding & agent
- Multimodal GraphRAG models missing and contradictory evidence for storm damage assessment — JeremyCMorgan · 2026-10-28
- Vibe coding in real life: 20 hours of personal-project work done in 2 — gleech · 2026-10-28
- LangChain open-sources Content Studio, a Slack design agent, and shares its harness design — BraceSproul · 2026-10-28
- "If AI can do it, humans shouldn't": team lets AI agent review PRs — Yuchenj_UW · 2026-10-28
- Sequoia, Citi and OpenAI launch No Limit: build a poker bot in 60 minutes, $100K grand prize — polynoamial · 2026-10-28
- Nyxis: a Lean framework with formally proven authorization safety for AI-written backends — udmrzn · 2026-10-28