AI 编程圈最近有个越来越响的口号：让形式化验证给模型写的代码做数学证明，做到「没有 Bug」。一篇 11 月 3 日挂上 arXiv 的论文，把这条流水线的成绩单拆开了。论文标题是《Verified