Un equipo de UC Berkeley lanzó Vero el 13 de agosto de 2026 — el primer benchmark para evaluar si los agentes de IA pueden producir software formalmente verificado a nivel de repositorio. El benchmark genera tanto implementaciones Lean 4 como pruebas verificadas por máquina que demuestran que las implementaciones satisfacen sus especificaciones. El agente de frontera más fuerte resuelve completamente solo 27 de 43 instancias y cierra cero especificaciones en los repositorios más difíciles.

Las 43 instancias de Vero se obtienen de repositorios de código real escritos originalmente en Python, Dafny, Verus y Coq, abarcando protocolos criptográficos hasta sistemas distribuidos. Cada instancia es un proyecto Lean 4 multi-módulo autónomo. Los curadores congelan tres capas — tipos de datos compartidos, firmas de API y especificaciones formales — y el agente escribe implementaciones y descarga pruebas. Cada instancia fue traducida manualmente a Lean 4 sin verdad fundamental en línea, evitando contaminación de datos de entrenamiento.

El benchmark se ejecuta en dos modos. El modo solo-prueba proporciona una implementación de referencia; el agente debe probar cada especificación contra ella. El modo código-y-prueba retiene la referencia y el agente escribe ambos desde cero. El arnés de calificación renderiza un proyecto Lean limpio de la fuente congelada, superpone los cuerpos de prueba del agente, compila con Lake y verifica el conjunto de axiomas de cada prueba contra una lista de permitidos. Una prueba con fugas de marcador `sorry` o axioma extranjero no cuenta. La CLI es simple: `vero run benchmark=bankledger agent=claude mode=proof` escribe informes por especificación con desgloses de axiomas en `agent_runs/<run>/eval/<name>/report.md`.

El benchmark anterior a nivel de función VERINA — del mismo autor principal — mostró que OpenAI o3 logró 72.6% de exactitud de código, 52.3% de solidez de especificación y 4.9% de éxito en pruebas en un único ensayo por tarea. Vero cuestiona si los agentes mantienen opciones coherentes de implementación y prueba en repositorios multi-módulo, no solo en límites de función. La respuesta: incluso los agentes más fuertes fallan en más de un tercio de las instancias y colapsan en las más difíciles.

En lugar de silenciar errores de benchmark, Vero proporciona espacios formales para que los agentes demuestren que una especificación es insatisfacible o que el código de referencia es incorrecto. Esto convirtió errores latentes de curación en hallazgos verificados por máquina durante la construcción — una técnica directamente aplicable a canalizaciones de CI en flujos de trabajo de generación de código donde las especificaciones pueden estar mal declaradas en lugar de que sea culpa del agente.

La síntesis de pruebas colapsa cuando los límites de módulos introducen dependencias entre archivos. Los agentes no logran mantener coherencia entre las opciones de implementación en un archivo y las obligaciones de prueba en otro. La tasa de 27/43 resoluciones completas obscurece la verdad más dura: cero especificaciones cerradas en las instancias más difíciles. Los agentes alcanzan un límite que más prompts o presupuesto de tokens no va a superar.

Si está evaluando agentes de generación de código para canalizaciones críticas de seguridad, "¿compila y pasa pruebas?" no es suficiente. Vero proporciona un arnés reproducible para agregar "¿cierra sus pruebas sin sorry?" a su conjunto de evaluación, disponible hoy en Python 3.10 con Lean 4.29.1.