Vero 把程式代理推至整個 Lean 4 儲存庫，最強設定只完整解出 27／43 題

Vero 將「驗證程式生成」由單一函式擴展到完整儲存庫：43 個 Lean 4 專案取材自 Python、Dafny、Verus 與 Coq 程式庫，合計包含 743 個待實作 API、2,705 條形式規格，題材橫跨密碼協定、共識系統、解析器及資料結構。每題固定資料型別、API 介面與規格；代理必須填入實作，再為所有規格產生可由 Lean 核心檢查的證明。

評測分成 proof-only 與 code-and-proof。前者提供參考實作，後者容許代理改寫演算法，因此可能選擇較容易歸納的版本，卻也可能令跨模組證明失效。為阻止以新增公理或竄改題目取巧，評分器只抽取指定區域的修改、在乾淨副本重建專案，並檢查證明所依賴的公理。基準亦接受「規格不可滿足」或「參考實作錯誤」的正式反證，避免把資料缺陷算成模型失敗。

作者以 Codex 和 Claude Code 搭配四組前沿模型設定測試；最佳的 GPT-5.5 xhigh 在 code-and-proof 模式完整解出 27／43 題，仍有 10 題在兩種模式下都未被任何設定攻破。失敗集中於跨模組不變量、協定一致性及自訂數學理論：代理常逐條嘗試局部證明，卻未先建立可重用的引理庫。

這使 Vero 比一般「測試是否通過」更接近安全關鍵軟體的驗證工作，但不能直接代表日常程式開發能力。資料只有 43 個人工轉寫專案，結果亦受代理工具、推理預算與 Lean 經驗影響；下一步應觀察不同團隊能否重現排名，以及代理能否主動規劃跨檔案引理而非只延長搜尋。