Vero 构成：43 个 Lean 4 仓库、743 个 API、2705 条规约
dawnsongtweets · x · 2026-08-23
Vero 由 43 个多模块 Lean 4 实例组成，从 Python、Dafny、Verus、Coq 真实仓库中策划而来，每个实例包含：固定的数据类型与 API 签名（共 743 个打分 API）、人工策划的形式化规约（共 2,705 条）、每个 API 的参考实现；领域覆盖密码协议、智能合约、分布式系统与数据结构。另有半自动化策划管线，可扩展到新的源语言。
所属事件:Dawn Song 团队发布首个仓库级形式化验证基准 Vero(9 条相关)→
「研究」频道最新
- SubQ 开源 Decision LCR:72K-115K 长文决策基准,自研模型领先 — ryanallred · 2026-10-16
- 「特征不是神经网络基本单位」：可解释性范式之争再升温 — MoonL88537 · 2026-10-16
- FOMO-Dex 力控遥操作：机器人学会拿薄卡片、拧螺丝 — HaozhiQ · 2026-10-16
- 机制可解释性新假设：神经网络从训练第一步就开始泛化 — burny_tech · 2026-10-16
- 普林斯顿 AI 实验室启动新研究计划：确保自主系统符合人类意图 — LakeBrenden · 2026-10-16
- UbiComp 2026 论文 OrganicHAR：让传感器「发现」活动而非识别预设标签 — mynkgoel · 2026-10-16