Výzkumníci představili benchmark Vero, první test, který hodnotí, zda AI agenti zvládnou vytvořit implementaci i strojově ověřený důkaz její správnosti napříč celými repozitáři. Obsahuje 43 více-modulových úloh z reálných projektů v jazycích Python, Dafny, Verus a Coq, od kryptografických protokolů po distribuované systémy. Každá úloha má předem daná API rozhraní, ručně připravené formální specifikace a referenční implementace. Autoři přidali i auditní mechanismus, který agentům umožňuje formálně dokázat nesplnitelnost specifikace nebo chybu v referenčním kódu, čímž se opravují skryté chyby v datech. Nejsilnější z testovaných agentů s přístupem k nástrojům Lean vyřešil pouze 27 ze 43 úloh a u nejtěžších repozitářů neuzavřel žádnou specifikaci. Benchmark, pipeline i vyhodnocovací nástroje jsou volně dostupné.
