EthSystems completa la verificación formal del pool de privacidad, cubriendo el bytecode de Sepolia

EthSystems, una organización de tecnología de privacidad de Ethereum, ha anunciado que ha completado la verificación formal de su pool de privacidad, abarcando desde las especificaciones escritas hasta el bytecode en la red de pruebas Sepolia. Durante el proceso de verificación se utilizaron diversas herramientas; los modelos, circuitos y hash utilizaron Lean, los contratos usaron Halmos y Kontrol, y las billeteras emplearon Aeneas y Verus, mientras que los verificadores y el despliegue se comprobaron mediante reconstrucción byte a byte. Se ha verificado que el doble gasto y la conservación del valor han sido validados por la máquina de teoremas Lean. Se encontraron un total de 6 problemas durante la verificación, de los cuales 3 se debieron a las herramientas de verificación en sí. El equipo también enumeró las suposiciones de las que aún dependen, incluyendo la ausencia de colisiones en los hashes, que los verificadores rechazarán pruebas falsas y que el comportamiento del contrato es consistente con el modelo.