Vitalik Buterin, cofundador da Ethereum, publicou a 18 de maio uma análise aprofundada sobre o estado e as perspetivas da verificação formal (Formal Verification), defendendo que a verificação formal apoiada por IA se tornará “a forma final do desenvolvimento de software” e apontando que a Ethereum será uma parte importante da arquitetura futura de “core de segurança”.
Os princípios centrais da verificação formal e os casos de uso
Conforme confirmado no artigo de Vitalik, a verificação formal é particularmente adequada para cenários em que “o objetivo é muito mais simples do que a implementação”; ele enumera, de forma explícita, quatro componentes tecnológicos centrais para o próximo ciclo de atualizações da Ethereum:
Assinaturas resistentes a ataques quânticos: já existe trabalho de verificação formal para variantes de assinaturas SPHINCS
Sistema de provas STARK: o projeto Arklib dedica-se à criação de uma implementação STARK totalmente sujeita a verificação formal
Algoritmo de consenso tolerante a falhas bizantinas: neste momento está a trabalhar na especificação e na demonstração formal das propriedades de segurança do consenso em Lean
ZK-EVM: o projeto evm-asm tem como objetivo criar uma implementação EVM com verificação formal completa (escrevendo diretamente em linguagem assembly RISC-V）
Vitalik cita a perspetiva de Yoichi Hirai, descrevendo este método como “a forma final do desenvolvimento de software”.
Direção de evolução da arquitetura de “core de segurança” descrita por Vitalik
Conforme confirmado no artigo de Vitalik, ele descreve o padrão de evolução futura da arquitetura de software:
Core de segurança: fortalecido continuamente através de métodos formais, suportando o mais alto nível de confiança; Vitalik afirma de forma explícita que a Ethereum, o núcleo de um sistema operativo e aplicações relacionadas com a Internet das Coisas irão tornar-se o core de segurança.
Borda insegura: os componentes de borda executam-se em ambiente sandbox, recebendo os mínimos privilégios necessários para concluir o trabalho; se um componente de borda falhar, o core de segurança fornece proteção.
Limitações de confirmação e modos de falha da verificação formal
Vitalik admite que a verificação formal não é uma solução para tudo; ao citar o trabalho de investigadores como Nadim Kobeissi (Cryspen), confirma três tipos principais de modos de falha: omissões de verificação (verifica apenas parte do código, enquanto a parte não verificada contém falhas críticas); omissões na especificação (erros na própria norma de segurança ou suposições incorretas na prova); ataques de canal lateral (ataques de side-channel na fronteira entre hardware e software, difíceis de serem capturados pelos modelos existentes).
Vitalik sublinha que “correção comprovável” valida, na essência, a consistência intrínseca entre intenções expressas, e não uma correspondência absoluta com as intenções reais dos humanos.
Ferramentas de verificação formal com apoio de IA
Conforme confirmado no artigo de Vitalik, as ferramentas disponíveis incluem: Lean (linguagem de provas matemáticas, com verificação automática de teoremas); Claude e Deepseek 4 Pro (Vitalik confirma que são suficientes para escrever provas em Lean); Leanstral (um modelo de pesos abertos com 119 mil milhões de parâmetros, afinado especificamente para escrever em Lean, capaz de correr localmente, com desempenho nos testes de referência superior ao de muitos modelos genéricos ainda maiores).
Perguntas frequentes
Porque é que Vitalik considera que a Ethereum deve tornar-se um “core de segurança”?
Conforme o artigo de Vitalik, a Ethereum é semelhante ao núcleo de um sistema operativo, suportando o mais elevado nível de confiança no processo de digitalização da sociedade. Ele indica que o objetivo do desenho de um core de segurança é fazer com que a sua segurança atinja um padrão que não permita a proliferação de código com falhas, e que toda a capacidade computacional adicional trazida pela IA deve ser canalizada para aumentar a segurança do core de segurança.
Porque é que a verificação formal é particularmente adequada para tecnologias como STARK e ZK-EVM?
De acordo com a análise de Vitalik, a característica comum destas tecnologias é que “o objetivo é muito mais simples do que a implementação” — as suas propriedades de segurança podem ser definidas de forma clara em linguagem matemática, mas a implementação concreta é extremamente complexa, exatamente o tipo de cenário em que a verificação formal pode ter maior impacto.
Como é que Vitalik recomenda que os programadores usem, na prática, a verificação formal com apoio de IA?
Conforme o artigo de Vitalik, ele recomenda que a IA escreva código Lean e provas matemáticas, ficando ao utilizador apenas verificar se as afirmações provadas correspondem ao esperado, sem necessidade de escrever manualmente o exaustivo código de prova de base. Ele confirma que Claude, Deepseek 4 Pro e Leanstral são as principais ferramentas disponíveis atualmente.
Aviso legal: As informações contidas nesta página podem provir de fontes externas e têm caráter meramente informativo. Não refletem os pontos de vista nem as opiniões da Gate e não constituem qualquer tipo de aconselhamento financeiro, de investimento ou jurídico. A negociação de ativos virtuais envolve um risco elevado. Não se baseie exclusivamente nas informações contidas nesta página ao tomar decisões. Para mais detalhes, consulte o
Aviso legal.
