UC Berkeley 团队发布 Vero 基准：测试 AI 智能体能否构建形式化验证的软件仓库

来源：AI HOT 精选·2026-09-02 10:28发布时间待核实

UC Berkeley 等机构发布 Vero，据称是首个要求智能体在仓库级同时编写实现与证明的基准，含 43 个多模块 Lean 4 实例、743 个计分 API 和 2705 条形式化规范。