Benchmark Vero de Berkeley: en el mejor de los casos, solo 27 de 43 proyectos resueltos
El laboratorio RDI de Berkeley publicó el benchmark Vero: agentes de IA escriben implementación y prueba formal en repositorios Lean 4, la mejor tasa de acierto por especificación llega al 87,3%, pero solo 27 de los 43 proyectos se resuelven por completo.