用一句话指令驱动 Aristotle 验证 Ibex RISC-V CPU 乘除指令

作者用团队开发的 Aristotle AI 定理证明器，通过 MCP 接入 Claude、Codex 等 agent，以一句自然语言指令形式化验证 Ibex RISC-V CPU 全部乘法与除法指令的功能正确性。验证过程将 RTL 实现与 SAIL RISC-V 形式规范（SVA）逐条比对，由 Aristotle 自动编排并逐条报告属性 PROVED；安装后注册 MCP server 即可使用。