用 Claude 证明内存安全等价,一次性挖出大量 PHP 深层 bug

jd_pressman · x · 2026-10-23

gf256 团队展示了一种用 AI 辅助形式化验证挖 bug 的新路子:先把代码编译到 RISC-V、x86 或 LLVM IR,然后用 Claude 对 ASAN 与非 ASAN 两个版本做等价性证明,验证其在所有输入下行为一致,从而批量找出内存安全 bug。

gf256 称这一方法找到了"大量"bug,是迈向发现全部内存安全 bug 的重要一步。jdpressman 在讨论中补充:形式化验证长期被放弃不是因为不可行,而是太费人力,而学术界的验证理论与工具一直在进步——AI 正在把这层人力瓶颈打掉,这可能是形式化方法复兴的拐点。