Harmonic 推出 Aristotle:可机器验证证明软件正确性的 AI agent
satnam6502 · x · 2026-09-10
帖子推荐 Harmonic 的形式化验证产品 Aristotle——一款「能证明软件正确」的 AI agent,主打将获 IMO 金牌水平的推理能力应用于软件、硬件与数学的形式化验证,每个输出都附带机器可检验的证明。
产品特点:
- 全 agentic:给它英文描述的问题,可从零证明并形式化,也可直接在 Lean 项目或代码仓库里工作、编辑文件
- 代码可入库:大规模形式化项目的负责人越来越多地无需修改就接受 Aristotle 的代码贡献
- 官网同时推出 100 万美元研究资助计划(Research Grant Program)
「编程与Agent」频道最新
- 仅 4B 参数纯 RL 训练,FrogNano 声称达成仓库级编程能力 — burkov · 2026-09-10
- Instinct 推出 Trusted Person 网络，个人 AI 助手之间可直接协商 — mon__lim · 2026-09-10
- diagram-design 技能让 Codex 与 Claude Code 一次生成 39 种图表 — daniel_mac8 · 2026-09-10
- Simular 旧金山办 CUA 派对,热议 2027 年计算机 Agent 会不会到 AGI — xwang_lk · 2026-09-10
- Harrison Chase：LLM 擅长写代码将引爆 computer use 普及 — hwchase17 · 2026-09-10
- 开源 Chrome 扩展：浏览器 agent 换标签页也能后台继续干活 — Silly_Entertainer92 · 2026-09-10