安全研究员豪赌：2028 年前 AI 无法形式化验证 Linux 内核等关键软件

JeffLadish · x · 2026-10-23

安全研究员 S1r1u5 向 rauchg 发起公开对赌，押注网络安全的攻防格局本质上是「进攻占优」：即使到 2028 年底，AI 也无法对 chromium、Firefox、Linux 内核、nginx、next.js、Apache 等核心软件（含全部依赖）完成形式化验证，否则认输。他还提出另一个更激进的对赌：即使到 2028 年后，自己或其他安全研究员仍会持续发现软件漏洞。Jeff Ladish 转发并表示愿意下注，认为观点要用真金白银检验。