伯克利 Vero 基准测仓库级形式验证

伯克利 RDI 实验室发布了 **Vero**,首个仓库级 Lean 4 形式化验证代码生成基准。它要求智能体在多模块项目里同时完成实现与证明，并始终保持代码、证明、构建三者一致——此前同类基准基本停在单定理或单函数层面。题面共 43 个项目，移植自 Python、Dafny、Verus、Coq 代码，覆盖 743 个 API 与 2705 条规范。

内核结果：**最强配置只完全解决 27/43 个实例**。更关键的是同一模型（GPT-5.5 加 Codex）仅把推理档位从 medium 调到 xhigh,解决数就从 2 跳到 27,思考预算的边际收益远未饱和。而单条规范通过率能到 87.3%,落到整仓口径只剩 27 个——量出了单点能力和工程完成度之间的具体宽度。

💡 为什么值得看Lean 4 项目完成度差距被量化，证明能力与工程能力脱节。