O co-fundador do ethereum, Vitalik Buterin, propôs uma nova linguagem de programação. Ela seria compilada diretamente em Lean ou HOL, outro assistente de prova formal.
A ideia visa preencher uma lacuna específica na forma como as pessoas leem a saída da IA. A inteligência artificial produz cada vez mais blocos grandes de provas automatizadas, muitas vezes mais rápido do que qualquer equipe humana poderia escrevê-las à mão. Poucos leitores conseguem confirmar rapidamente o que essas provas realmente estabelecem.
Uma linguagem criada apenas para revisores de IA
Lean é um assistente de prova, um software usado por matemáticos e engenheiros para escrever provas que um computador pode verificar linha por linha. Pesquisadores do ethereum já o utilizam para verificar código criptográfico e lógica de consenso. Assistentes de prova existem há quase 60 anos, mas o campo permaneceu como uma área de interesse restrito.
Em seu post, Buterin argumentou que os passos internos de uma prova têm apenas um requisito: a correção matemática, nada mais. Os leitores nunca inspecionam diretamente essa maquinaria. Definições e teoremas funcionam de forma diferente, pois os seres humanos leem essas partes para entender o que um trecho de software realmente garante.
Buterin explorou uma divisão relacionada em um post de blog em maio. Lá, uma prova matemática mostra que código de baixo nível eficiente corresponde a uma especificação separada e legível, de modo que uma única auditoria cobre ambas as versões ao mesmo tempo.
Seu timing também coincide com o próprio esforço de reconstrução da Ethereum, que possui um apelido separado, o Lean Ethereum roadmap. Pesquisadores, ao mesmo tempo, estão desenvolvendo um formally verified ZK-EVM, uma versão com comprovação de zero-knowledge da máquina virtual da Ethereum (EVM), usando métodos comparáveis.
IA escreve as provas, humanos verificam as afirmações
Modelos de linguagem de grande porte já conseguem escrever provas em Lean utilizáveis. Buterin nomeou o Claude e o Deepseek 4 Pro como ferramentas capazes, juntamente com o Leanstral, um modelo menor ajustado especificamente para Lean. Um exemplo de projeto é o evm-asm, uma implementação da EVM verificada contra uma referência legível. Essa capacidade ecoa as habilidades de raciocínio exibidas pelos desenvolvedores em um recente desafio de Buterin. Os testadores resolveram esse desafio em poucas horas.
Os stakes vão além da conveniência, no entanto. Pesquisadores de segurança rastrearam um aumento nas tentativas de exploração assistidas por IA este ano. Código formalmente verificado oferece uma defesa contra essa tendência. Uma linguagem de especificação mais amigável permitiria aos desenvolvedores auditar afirmações sem precisar navegar pela prova circundante.
Além dos círculos de pesquisa da ethereum
Buterin continua testando essas ideias publicamente, pois recentemente demonstrou um outdoor anônimo construído com provas de conhecimento zero. A demonstração mostrou como afirmações verificáveis podem passar de repositórios de pesquisa para produtos funcionais. Pesquisadores também começaram a verificar formalmente clientes de consenso em Lean para detectar bugs precocemente.
Ainda assim, a direção ecoa um padrão familiar: separe o código rápido das afirmações legíveis, depois prove que os dois coincidem.
Ainda não existe nenhum protótipo da nova linguagem, e Buterin deixou a sintaxe exata em aberto. Os desenvolvedores podem convergir para um padrão compartilhado ou optar por vários dialetos incompatíveis. Essa escolha pode determinar quão rapidamente o código verificado por IA chegará aos sistemas de produção.