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 teórica de juegos de los protocolos de blockchain. En resumen: la herramienta verifica si los incentivos en un protocolo hacen que hacer trampa no valga la pena.

Los protocolos necesitan 3 tipos de seguridad: • Criptográfica: ¿Son fuertes tus claves/contraseñas? • Implementacional: ¿Hay errores en el código? • Teórica de juegos: ¿Están alineados los incentivos para que hacer trampa no compense? Esa última es crucial, pero a menudo se ignora.

La seguridad teórica de juegos se trata de 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 prueba formal y automáticamente la seguridad teórica de juegos utilizando solucionadores SMT. El documento introduce un algoritmo composicional de "divide y vencerás" que escala a millones de nodos, intercalando la generación de modelos y el análisis para mayor eficiencia.

Por qué esto es importante: Ahora podemos demostrar de manera automática, formal y a gran escala que los incentivos de un protocolo de blockchain hacen que hacer trampa sea irracional, antes de su implementación.