¿Verificación formal? ¿Qué es? Aprende más 🧵
Billones de dólares se encuentran en cadenas de bloques. Un error de consenso = drenaje instantáneo. Las pruebas pueden encontrar errores, pero no pueden demostrar que sean imposibles. La verificación formal de los protocolos basados en DAG cambia ese juego.
La verificación formal modela un protocolo como una máquina de estado y permite a un probador comprobar exhaustivamente cada transición, no solo una muestra de prueba.
¿La parte difícil? Las pruebas son lentas de escribir. La idea de Sonic: dividir los protocolos en bloques de construcción reutilizables en lugar de reinventar las pruebas cada vez.
Sonic Labs acaba de abrir una biblioteca TLA+ que demuestra matemáticamente la seguridad de DAG-Rider, Hashgraph, Bullshark, Aleph y más, sin muro de pago, sin acuerdos de confidencialidad.
Dijkstra: "Las pruebas de programas pueden mostrar la presencia de errores, pero nunca su ausencia". Las pruebas te dan la parte de ausencia.
La biblioteca divide las cosas en dos:
• Construcción 🌳 DAG
• Ordenamiento / elección 🗳️ de líderes
Cada bloque tiene su propia especificación + prueba verificada por máquina.
Se necesitaron ~ 14 meses-persona en 5 investigadores para modelar 5 protocolos. Agregar un sexto ahora lleva días, no meses.
El trabajo debutó en NASA Formal Methods 2025. Si es lo suficientemente robusto para cohetes, ¡probablemente sea bueno para Sonic!
Advertencia: estas pruebas cubren la seguridad (sin tenedores, sin gastos dobles). No solucionan los ataques económicos o de vida, pero eliminar clases enteras de errores de seguridad sigue siendo una gran victoria.
TL; DR — Las listas de verificación de auditoría son de 2020. Las pruebas componibles y de código abierto son 2025. Hagamos que "probadamente seguro" sea el valor predeterminado en las criptomonedas.
Blog →
Código →
4.82 K
35
El contenido al que estás accediendo se ofrece por terceros. A menos que se indique lo contrario, OKX no es autor de la información y no reclama ningún derecho de autor sobre los materiales. El contenido solo se proporciona con fines informativos y no representa las opiniones de OKX. No pretende ser un respaldo de ningún tipo y no debe ser considerado como un consejo de inversión o una solicitud para comprar o vender activos digitales. En la medida en que la IA generativa se utiliza para proporcionar resúmenes u otra información, dicho contenido generado por IA puede ser inexacto o incoherente. Lee el artículo enlazado para más detalles e información. OKX no es responsable del contenido alojado en sitios de terceros. Los holdings de activos digitales, incluidos stablecoins y NFT, suponen un alto nivel de riesgo y pueden fluctuar mucho. Debes considerar cuidadosamente si el trading o holding de activos digitales es adecuado para ti según tu situación financiera.