Harmonic 工程师展示 Aristotle 形式验证成果

Harmonic 软件工程师 Satnam Singh 在格拉斯哥大学计算机系 CAKES Talk 上发表题为「为什么形式化验证世界正在火热」的研讨会。他展示其 AI 形式化验证系统 Aristotle 的两项成果：对照 SAIL 生成的 SystemVerilog 模型，机器验证了 Ibex RISC-V 核 MUL 乘法运算的正确性；并成功证明了 OpenTitan 硅根信任的 C 代码内存安全。

2026-10-30 ~ 2026-10-31 · 3 条相关

• Harmonic 工程师在格拉斯哥大学开讲：形式验证世界为何火热 — satnam6502 · 2026-10-30
• Aristotle 系统机器验证 Ibex RISC-V 核 MUL 运算正确性 — satnam6502 · 2026-10-31
• 用 AI 形式化验证系统 Aristotle 证明 OpenTitan 根信任 C 代码内存安全 — satnam6502 · 2026-10-31