Harmonic 的 Aristotle 模型扩展至 C 与 Verilog 代码的形式化验证
Harmonic expands its math-proving AI into C and Verilog code checks
AI 导读
Harmonic 于 10 月 27 日宣布，其数学证明 AI 模型 Aristotle 现在可验证 C 软件与 Verilog 芯片设计，通过将规格说明转为数学命题并在 Lean 4 中逐步构造形式化证明。
Harmonic 的 Aristotle 模型扩展至 C 与 Verilog 代码的形式化验证