Formal Vibefication：AI 如何打破形式化验证的成本困局

文章指出形式化验证技术（如 CompCert、seL4、HACL*）早已在生产环境使用，但受制于编写成本高、人才稀缺、性能与正确性取舍三大约束，始终未能进入普通工程团队。作者认为 AI 正在打破这一成本壁垒，使验证软件从学术特例走向常规实践。