- Vitalik defende verificação formal assistida por IA para blindar contratos inteligentes
- Cofundador do Ethereum cita STARKs, ZK-EVMs e consenso como alvos prioritários
- Proposta divide software em camada periférica insegura e núcleo crítico auditável
O cofundador do Ethereum, Vitalik Buterin, publicou um ensaio em que rebate o pessimismo crescente sobre o futuro da segurança digital. Para ele, a combinação entre inteligência artificial e verificação formal pode transformar a forma como código crítico é escrito e dar vantagem definitiva ao lado defensor em uma era de ataques cada vez mais sofisticados.
A provocação responde a uma tese que ganhou força em fóruns de cibersegurança, a de que ferramentas de IA capazes de encontrar bugs em massa tornariam impossível construir sistemas verdadeiramente sem confiança. Buterin discorda.
“Tenho uma visão muito mais otimista, e a verificação formal assistida por IA é boa parte da razão”, escreveu.
O que muda com verificação formal
Verificação formal é a prática de escrever provas matemáticas sobre o comportamento de um software. Em vez de testar e torcer para que nenhum bug apareça, o desenvolvedor demonstra, com rigor lógico, que o código se comporta conforme o esperado em todas as condições possíveis.
A técnica existe há décadas, mas sempre esbarrou no mesmo gargalo, escrever essas provas manualmente é lento e exige especialistas escassos. Aqui entra a virada proposta por Buterin. A IA assume tanto a geração do código quanto a redação das provas, restando ao humano apenas validar se aquilo que está sendo provado corresponde, de fato, à intenção original do projeto.
O pesquisador Yoichi Hirai, citado pelo próprio Buterin, descreve esse arranjo como “a forma final do desenvolvimento de software”. A diferença em relação ao paradigma atual é qualitativa, sai a confiança probabilística baseada em testes, entra a certeza matemática.
Frentes em andamento no ecossistema Ethereum
Buterin listou áreas onde a abordagem já está sendo aplicada. Assinaturas resistentes a computadores quânticos, sistemas de prova STARK, algoritmos de consenso e ZK-EVMs aparecem entre os alvos prioritários. São camadas em que o objetivo de segurança é fácil de descrever, ainda que a implementação seja imensamente complexa.
O projeto Arklib, por exemplo, busca uma implementação STARK totalmente verificada. O evm-asm reescreve a Máquina Virtual do Ethereum em assembly RISC-V, com prova matemática de equivalência a uma referência legível por humanos. Protocolos de consenso bizantino também estão sendo formalizados na linguagem Lean.
O argumento técnico tem leitura direta para o investidor: bugs em contratos inteligentes representam o principal vetor de perdas no setor. Apenas em 2026, exploits em pontes e protocolos somaram centenas de milhões de dólares caso recente foi a ponte Verus, alvo de ataque que elevou o rombo acumulado em bridges a US$ 329 milhões. Reduzir esse tipo de risco fortalece a tese de DeFi como infraestrutura financeira séria.
Os limites que o próprio Vitalik reconhece
O texto evita o triunfalismo. Buterin enumera falhas conhecidas do método: provas podem cobrir apenas parte do sistema, deixando trechos críticos sem verificação; o desenvolvedor pode esquecer de especificar propriedades relevantes, a própria especificação formal pode estar errada; e ataques de canal lateral em hardware contornam qualquer correção matemática do software.
“Corretude provável não prova que o software é correto da forma como a maioria dos humanos entende corretude”, escreveu.
A verificação formal funciona, segundo ele, como um conjunto de afirmações redundantes que precisam ser compatíveis entre si, não como uma garantia absoluta contra todo tipo de falha.
Visão de software em duas camadas
A proposta culmina em um modelo arquitetônico dividido. Na periferia, uma camada insegura roda funções de menor risco em sandboxes, com permissões mínimas. No núcleo, um conjunto pequeno e auditado abriga o que é crítico: o próprio Ethereum, kernels de sistemas operacionais e infraestrutura sensível de IoT.
Esse núcleo permaneceria deliberadamente enxuto e submetido a verificação formal agressiva, viabilizada pela capacidade de cálculo da IA. “Os defensores finalmente têm uma chance de vencer, decisivamente”, concluiu, mencionando a experiência da Mozilla ao endurecer sua base de código contra ferramentas ofensivas automatizadas.
A discussão chega em momento sensível para o Ethereum. Com pressão sobre o preço do ETH e tesourarias corporativas acumulando 7,3 milhões de ETH, a narrativa de robustez técnica volta ao centro do debate institucional sobre a rede. Para o investidor brasileiro exposto a DeFi via exchanges locais, segurança matemática do código é o que separa um ativo de infraestrutura de uma aposta especulativa.
