Una prueba en Lean afina el trabajo de Ethereum sobre confirmación rápida
Francesco D’Amato describe una prueba de seguridad verificada por computadora y un error en fork choice detectado al adaptar el modelo a próximos cambios.
El investigador de Ethereum Francesco D’Amato informa que la Fast Confirmation Rule ya cuenta con una prueba de seguridad en Lean, un asistente de demostración que verifica argumentos matemáticos formales. Su relato describe cómo varios agentes realizaron gran parte del trabajo de verificación durante varios días, con un modelo que seguía de cerca la especificación de consenso.
La confirmación rápida es distinta de la finalidad. D’Amato describe una confirmación en unos 24 segundos bajo supuestos adicionales, en lugar de esperar aproximadamente 13 minutos para alcanzar la finalidad. La prueba aborda la seguridad bajo esos supuestos; no elimina la necesidad de comprenderlos.
Según el investigador, adaptar el modelo a los próximos cambios de Gloas dejó al descubierto un error sutil en la selección de la cadena. Afirma que se corrigió la especificación y que luego la verificación actualizada se completó con éxito. Es un ejemplo concreto de cómo comprobar que una propiedad existente se mantiene cuando cambia el protocolo que la rodea.
Perspectiva de ETH Canal: las herramientas que aceleran la investigación son útiles cuando sus resultados se pueden verificar. Para los equipos que dependen de los tiempos de confirmación, el siguiente paso valioso es comprender los supuestos de la regla y el comportamiento exacto que necesita su producto. Un tiempo estimado de confirmación corto no debería convertirse de forma implícita en una promesa de liquidación definitiva.