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

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