O cofundador do Ethereum, Vitalik Buterin, propôs uma nova linguagem de programação. Ela compilaria diretamente para Lean ou HOL, outro assistente de prova formal.
A ideia visa uma lacuna específica em como as pessoas leem a saída da IA. A inteligência artificial produz cada vez mais grandes blocos 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 Construída Apenas para Leitores de Provas de IA
Lean é um assistente de provas, um software que matemáticos e engenheiros usam 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 uma busca de nicho.
Em sua postagem, Buterin argumentou que os passos internos de uma prova têm apenas um requisito. Esse requisito é a correção matemática, nada mais. Os leitores nunca inspecionam essa maquinaria diretamente. Definições e teoremas funcionam de maneira diferente, uma vez que os humanos leem essas partes para aprender o que um pedaço de software realmente garante.
Buterin explorou uma divisão relacionada em uma postagem de blog em maio. Lá, uma prova matemática mostra que um 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.
O tempo dele também se alinha com o próprio esforço de reconstrução do Ethereum, que tem um apelido separado, o roadmap Lean Ethereum. Enquanto isso, os pesquisadores estão construindo um ZK-EVM formalmente verificado, uma versão da máquina virtual do Ethereum (EVM) que pode ser provada por conhecimento zero, usando métodos comparáveis.
IA Escreve as Provas, Humanos Verificam as Alegações
Modelos de linguagem grandes já podem escrever provas Lean utilizáveis. Buterin nomeou Claude e Deepseek 4 Pro como ferramentas capazes, ao lado de Leanstral, um modelo menor ajustado especificamente para Lean. Um projeto exemplo é o evm-asm, uma implementação do EVM verificada contra uma referência legível. Essa capacidade ecoa as habilidades de raciocínio que os desenvolvedores demonstraram em um recente desafio de IA de Buterin. Os testadores resolveram esse desafio em poucas horas.
No entanto, os riscos vão além da conveniência. 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 que os desenvolvedores auditassem alegações sem ter que se aprofundar na prova circundante.
Além dos Círculos de Pesquisa do Ethereum
Buterin continua testando essas ideias em público, como ele recentemente demonstrou um outdoor anônimo construído com provas de conhecimento zero. A demonstração mostrou como alegações verificáveis podem passar de repositórios de pesquisa para produtos funcionais. Os 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: separar código rápido de declarações legíveis, e então provar que os dois correspondem.
Nenhum protótipo da nova linguagem existe ainda, 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 chega aos sistemas de produção.
Fonte: BeInCrypto
