Um time da UC Berkeley lançou Vero em 13 de agosto de 2026 — o primeiro benchmark para avaliar se agentes de IA podem produzir software formalmente verificado no nível do repositório. O benchmark gera tanto implementações Lean 4 quanto provas verificadas por máquina de que as implementações satisfazem suas especificações. O agente de fronteira mais forte resolve completamente apenas 27 de 43 instâncias e fecha zero especificações nos repositórios mais difíceis.

As 43 instâncias de Vero são originadas de repositórios de código reais escritos originalmente em Python, Dafny, Verus e Coq, abrangendo protocolos criptográficos até sistemas distribuídos. Cada instância é um projeto Lean 4 multi-módulo autossuficiente. Os curadores congelam três camadas — tipos de dados compartilhados, assinaturas de API e especificações formais — e o agente escreve implementações e descarrega provas. Cada instância foi traduzida manualmente para Lean 4 sem verdade terrestre online, prevenindo contaminação de dados de treinamento.

O benchmark executa em dois modos. Modo somente-prova fornece uma implementação de referência; o agente deve provar cada especificação contra ela. Modo código-e-prova retém a referência e o agente escreve ambos do zero. O harness de classificação renderiza um projeto Lean limpo da fonte congelada, sobrepõe os corpos de prova do agente, compila com Lake, e verifica cada conjunto de axiomas da prova contra uma lista de permissões. Uma prova com vazamento de placeholder `sorry` ou axioma estrangeiro não conta. A CLI é simples: `vero run benchmark=bankledger agent=claude mode=proof` escreve relatórios por especificação com desagregações de axiomas em `agent_runs/<run>/eval/<name>/report.md`.

O benchmark anterior em nível de função VERINA — do mesmo autor líder — mostrou o OpenAI o3 alcançando 72,6% de correção de código, 52,3% de solidez de especificação e 4,9% de sucesso em prova em uma única tentativa por tarefa. Vero questiona se agentes mantêm escolhas de implementação e prova coerentes em repositórios multi-módulo, não apenas em fronteiras de função. A resposta: até mesmo os agentes mais fortes falham em mais de um terço das instâncias e colapsam nos mais difíceis.

Em vez de silenciar erros de benchmark, Vero fornece slots formais aos agentes para provar uma especificação insatisfeita ou código de referência incorreto. Isso transformou bugs de curadoria latentes em achados verificados por máquina durante a construção — uma técnica diretamente aplicável a pipelines de CI em fluxos de trabalho de geração de código onde especificações podem estar mal colocadas em vez do agente culpado.

A síntese de prova colapsa quando limites de módulo introduzem dependências entre arquivos. Agentes falham em manter consistência entre escolhas de implementação em um arquivo e obrigações de prova em outro. A taxa de 27/43 resoluções completas obscurece a verdade mais dura: zero especificações fechadas nas instâncias mais difíceis. Agentes atingem um teto que mais prompt ou orçamento de token não vai limpar.

Se avaliando agentes de geração de código para pipelines de segurança crítica, "isso compila e passa em testes" não é suficiente. Vero fornece um harness reproduzível para adicionar "isso fecha suas provas sem sorry" ao seu conjunto de avaliação, disponível hoje em Python 3.10 com Lean 4.29.1.