Victor Taelin：AI 让证明成本骤降，形式化验证正迎来爆发

Victor Taelin 解释形式化验证为何正在爆发：随着 AI 能力增强，构造证明的成本持续下降，而 AI 越强大，漏洞被利用的成本与风险也越高。形式化证明能够消除漏洞，证明检查本身还是完美的数学与编程 RL 奖励信号，剩下的关键是经济学问题。