形式化验证的信任危机：当“绝对正确”的证明器出现裂痕

本文由计算机科学泰斗、Isabelle定理证明器创始人Lawrence Paulson撰写，深刻剖析了形式化验证领域的“阿喀琉斯之踵”。虽然形式化验证被视为保障芯片设计、操作系统及AI算法安全的“黄金标准”，但Paulson指出，证明器本身也是软件，内核漏洞或逻辑定义错误可能导致错误的数学定理被验证为“真”。文章通过具体案例警示业界，过度依赖自动化证明工具存在巨大隐患，必须保持对工具局限性的清醒认知与严格的人工审查机制。