El bug de @Zcash llevó a Ironwood, la verificación formal del circuito de pago Orchard. Lo amo y lo apoyo. También quiero enfatizar que @Starknet ha estado haciendo esto —verificación formal— desde hace más de 5 años. Es importante apoyar grandes proyectos como Zcash por reaccionar rápidamente, como en este caso. También es importante reconocer proyectos que son futuros seguros y están por delante de la curva, como Starknet. (Detalles en el artículo a continuación) He dicho con frecuencia que Starknet es ese sistema que ya tiene lo que otras cadenas afirman que tendrán pronto. Ha sido cierto en muchas cosas. Hemos estado a la vanguardia de muchas elecciones impopulares que ahora todos reconocen como importantes, incluyendo ZK-STARKs seguros contra la computación cuántica como la mejor solución para escalabilidad y privacidad, zkVMs ligeros (Cairo es el mejor), disponibilidad de datos Validium y verificación formal. La verificación formal significa que usas herramientas automatizadas como el sistema Lean para probar matemáticamente que tu código es seguro. Es muy difícil capturar cada aspecto de lo que significa que un código sea seguro, pero liderados por nuestro CTO @LiorGoldberg2 (co-creador del zkVM y lenguaje Cairo), llevamos más de 5 años haciendo esto. El primer artículo sobre verificación formal de afirmaciones relacionadas con ZK (el profesor Jeremy Avigad, Yoav Seginer y otros) demostró que el conjunto de restricciones polinómicas que definen la VM Cairo es correcto. Si has seguido las noticias recientemente, el bug descubierto recientemente por IA y ahora corregido en Zcash (otro proyecto que cofundé y del que estoy muy orgulloso y apoyo) tenía que ver con una restricción faltante. La decisión de verificar su código para descartar otros errores similares es el paso correcto. Ejecutar este tipo de verificación para la VM central de Cairo nos proporcionó, al equipo de StarkWare, certeza matemática de que no hay ninguna restricción faltante en nuestra VM Cairo. Por lo tanto, además de probar la VM central de Cairo, también hemos probado el sistema S-two STARK, parte del compilador, y muchas de las funciones en la biblioteca estándar de Cairo. ¿Se ha terminado el trabajo? No. Hay muchas otras cosas que pueden probarse formalmente. Pero estamos comprometidos a continuar probando formalmente todas las propiedades centrales relacionadas con la solidez y seguridad de nuestros sistemas. Es excelente ver que otros proyectos adoptan la verificación formal como una herramienta importante. Estoy orgulloso de que StarkWare haya liderado el camino en este aspecto también. Eso es lo que significa para nosotros una cadena de bloques futura segura. ¿Quieres saber más? Aquí tienes un informe detallado sobre nuestros esfuerzos de prueba con Lean en los últimos años.