Harmonic Aristotle 6小时证明 TorchLean C 代码 211/213 条性质

satnam6502 · x · 2026-10-28

Harmonic 宣布将形式化验证系统 Aristotle 引入代码验证，首发支持 C 与 Verilog，目标是验证 AI 生成的海量代码。

用户 @Robertljg 实测：把 Aristotle 指向 TorchLean 的 C runtime 代码，约 6 小时内证明了 213 条性质中的 211 条（涵盖内存安全、引用计数、功能正确性），配图显示 211 PROVED / 2 REFUTED。剩余 2 条被给出了一个 use-after-free 反例，涉及调用方引用计数不一致，团队正在复查所有权假设与证明材料，以确认到底哪些性质真正成立。