La semana pasada en OOPSALA '25, nuestros desarrolladores de Act presentaron una versión mejorada y escalable de CheckMate, un probador automatizado para verificar formalmente la seguridad de la teoría de juegos de los protocolos blockchain. En resumen: la herramienta comprueba si los incentivos de un protocolo hacen que no valga la pena hacer trampa.

Los protocolos necesitan 3 tipos de seguridad: • Criptográfico: ¿Son seguras sus claves/contraseñas? • Implementación: ¿Hay errores en el código? • Teoría de juegos: ¿Están los incentivos alineados para que hacer trampa no valga la pena? Este último es crucial, pero a menudo se ignora.

La seguridad de la teoría de juegos consiste en asegurarse de que incluso los actores racionales y egoístas prefieran seguir las reglas, porque desviarse cuesta más de lo que gana. Es la "economía" de la seguridad.

CheckMate demuestra formal y automáticamente la seguridad de la teoría de juegos utilizando solucionadores SMT. El documento presenta un algoritmo composicional de "divide y vencerás" que escala a millones de nodos, intercalando la generación y el análisis de modelos para la eficiencia.

Por qué esto es importante: Ahora podemos demostrar de forma automática, formal y a escala que los incentivos de un protocolo blockchain hacen que las trampas sean irracionales, antes de su implementación.