宋晓冬教授的Vero，论文和基准全部开源
现在的 AI 编程 Agent（比如 Codex、Claude Code）能生成代码，但不保证正确。测试能抓常见 bug，但抓不到边界 case 和安全漏洞。代码仓库（Repository）就是一个完整的工程项目。不是单个函数，而是一整套东西：几十个文件、几百个函数、模块之间互相调用，共同完成一件事Vero 给这个行业立了一个标杆，不是看你能写多少行代码，而是看你能不能用数学保证整个仓库的正确性。Vero 的评分逻辑是，100 条规范，99 条证了，1 条没证就 整个仓库失败。追求的是"数学上绝对正确"。目前 frontier Agent 离这个目标还有明显距离。AI 不是为了"正确"而写代码，它是为了"通过你的检查"而写代码。