¿Qué se necesita realmente para que Web3 sea confiable?

El episodio de la semana pasada del podcast @HeliosStaking contó con la participación de @RosuGrigore sobre verificabilidad, métodos formales y la construcción de sistemas comprobables para el futuro de la infraestructura descentralizada.

↓ Aquí lo que destacó:

De @NASA a la infraestructura blockchain: @RosuGrigore comenzó aplicando métodos formales a sistemas críticos para misiones en NASA. Hoy, esas mismas herramientas se están usando en blockchains que exigen corrección comprobable.

Cómo tomó forma Runtime Verification: @RosuGrigore fundó @rv_inc para llevar los métodos formales a sistemas del mundo real. Inicialmente rechazado por conferencias de testing y métodos formales, el término “runtime verification” redefinió el enfoque—combinando observación en tiempo de ejecución con garantías de corrección. Ahora, define toda una categoría de aseguramiento de sistemas.

Por qué importan las semantics: Sin semantics formales, los lenguajes de programación se vuelven objetivos móviles. Pi Squared usa el K Framework y Matching Logic para definir y razonar sobre el comportamiento de programas con precisión matemática.

Apoyo de @IOHK_Charles y @VitalikButerin: IOHK financió trabajos tempranos en la formalización de lenguajes en K. Vitalik otorgó subvenciones para verificar el protocolo Casper de Ethereum, Vyper, Uniswap y el contrato de depósito ETH2—algunos de los primeros esfuerzos de verificación formal en el espacio.

Verificabilidad sin orden: Pi Squared introduce una capa de liquidación descentralizada donde las afirmaciones—ya sean de rollups, agentes AI o exchanges—pueden ser verificadas de forma independiente y en paralelo. Sin necesidad de orden global. Solo prueba.

“Sin verificabilidad, no hay Web3.”

La corrección se vuelve portable.
La verdad se vuelve programable.