Ler no idioma original (inglês)
Ethereum Avança na Verificação de Consenso com Lean 4
A equipe de pesquisa do Ethereum está desenvolvendo um projeto chamado 'Etheorem' para implementar e verificar matematicamente as especificações de consenso das atualizações Fulu, Gloas e Heze usando Lean 4. Esta iniciativa visa minimizar os riscos associados a diferentes interpretações das mesmas especificações por diversos clientes.
Visão Geral do Projeto
A equipe de pesquisa do Ethereum está realizando um projeto significativo chamado 'Etheorem', que tem como objetivo implementar e verificar matematicamente as especificações de consenso das atualizações Fulu, Gloas e Heze utilizando o assistente de provas Lean 4. Este esforço busca reduzir o risco de divisões na cadeia que podem ocorrer quando múltiplos clientes interpretam as mesmas especificações de maneira diferente.
Objetivos do Etheorem
O principal objetivo do Etheorem é criar uma implementação funcional das especificações de consenso do Ethereum em Lean 4, avançando além de simples testes de código para validar matematicamente a lógica central. O projeto divulgou seu progresso por meio de uma postagem no Ethereum Research Forum pela Ethereum Protocol Fellowship (EPF) e pela equipe de pesquisa Invisible Garden.
Implementação Técnica
O Etheorem implementou com sucesso as especificações de consenso para as três atualizações. Ele pode executar transições de estado e lógica de escolha de fork, comparando seus resultados com vetores de teste de consenso oficiais do Ethereum. As principais características das atualizações incluem:
- Fulu: Especificações relacionadas à amostragem de disponibilidade de dados.
- Gloas: Elementos referentes à estrutura do leilão de carga de execução (ePBS).
- Heze: Recursos voltados para resistência à censura por meio de estruturas de listas de inclusão.
Técnicas de Verificação
O projeto utiliza a biblioteca SSZ (Simple Serialize), conhecida como SizzLean, para validar propriedades críticas necessárias para a serialização e desserialização de dados de consenso, além de cálculos de árvores de Merkle. A verificação checa se os dados serializados retornam ao seu valor original, garante que valores diferentes não compartilhem a mesma codificação e confirma que os tamanhos de codificação não excedem limites predefinidos.
A iniciativa também se concentra em reduzir discrepâncias entre o código verificado e o código de execução real, utilizando as mesmas definições de especificação em ambos os ambientes de verificação e execução. No entanto, é importante notar que essa verificação formal não substitui todo o ecossistema de clientes do Ethereum, e passar nos vetores de teste não garante estabilidade operacional ou prontidão para lançamento formal. O projeto planeja expandir seu escopo de prova no futuro.