Prova em Lean aprimora o trabalho de confirmação rápida do Ethereum

O pesquisador de Ethereum Francesco D’Amato relata que a Fast Confirmation Rule agora tem uma prova de segurança em Lean, um assistente de provas que verifica argumentos matemáticos formais. Seu relato descreve agentes realizando boa parte do trabalho de verificação ao longo de vários dias, com um modelo que segue de perto a especificação de consenso.

Confirmação rápida é diferente de finalização. D’Amato descreve uma confirmação em cerca de 24 segundos sob premissas adicionais, em vez de esperar aproximadamente 13 minutos pela finalização. A prova trata da segurança sob essas premissas; ela não elimina a necessidade de compreendê-las.

Segundo o pesquisador, a adaptação do modelo às próximas mudanças de Gloas revelou um bug sutil na escolha de bifurcação. Ele afirma que a especificação foi corrigida e que a verificação atualizada foi então concluída com sucesso. É um exemplo concreto de como verificar se uma propriedade existente se mantém diante de uma mudança no protocolo ao redor dela.

Perspectiva do ETH Canal: ferramentas de pesquisa mais rápidas são úteis quando seus resultados podem ser verificados. Para equipes que dependem dos tempos de confirmação, o próximo passo relevante é entender as premissas da regra e o comportamento exato de que seu produto precisa. Uma estimativa curta de confirmação não deve se transformar silenciosamente em uma promessa de liquidação definitiva.