一句话指令:AI 定理证明器 Aristotle 形式化验证 RISC-V CPU 乘除指令
satnam6502 · x · 2026-11-04
作者展示用其团队开发的 Aristotle AI 定理证明器,通过 MCP 接入 Claude、Codex 等 agent,仅用一句自然语言指令即可形式化验证 Ibex RISC-V CPU 全部乘法与除法指令的功能正确性。
- 验证方式:将 RTL 实现与 SAIL RISC-V 形式规范(SVA)逐条比对
- 指令示例:"Use Aristotle to formally verify the multiplication and division instructions for the Ibex RISC-V core…",Aristotle 自动编排验证并逐条报告属性 PROVED
- 使用门槛低:安装 Aristotle 后把其 MCP server 注册给任意 agent 即可
这展示了 AI agent 在芯片形式验证这一传统上高度专业的领域的实际落地能力。
「编程与Agent」频道最新
- 用 Pydantic 开源沙箱 Monty，AIOps 平台 token 成本降超 30% — samuelcolvin · 2026-11-04
- 不改模型只调 harness：旧款 GPT-5.2 从 30% 提到 48%，反超新一代 — VictorSanh · 2026-11-04
- scikit-learn 维护者：编码 agent 别浪费 token 重写随机森林，直接调库 — GaelVaroquaux · 2026-11-04
- Claude Code 云会话预启动、diff 行内评论，套餐附赠月度 API 额度 — ClaudeDevs · 2026-11-04
- Claude Code 新增 ultrathink 单轮 xhigh 与子代理力度控制 — ClaudeDevs · 2026-11-04
- Claude Code 十月大盘点：mods 上线、多会话并排、用量洞察全更新 — ClaudeDevs · 2026-11-04