Benchmark Vero de Berkeley: na melhor das hipóteses, só 27 de 43 projetos concluídos
O laboratório RDI de Berkeley lançou o benchmark Vero: agentes de IA escrevem implementação e prova formal em repositórios Lean 4, a melhor taxa de acerto por especificação chega a 87,3%, mas apenas 27 dos 43 projetos são resolvidos por completo.