Na semana passada, na OOPSALA '25, os nossos desenvolvedores Act apresentaram uma versão melhorada e escalável do CheckMate, um provador automatizado para verificar formalmente a segurança teórica dos jogos dos protocolos de blockchain. Em resumo: a ferramenta verifica se os incentivos em um protocolo tornam a trapaça não compensadora.

Os protocolos precisam de 3 tipos de segurança: • Criptográfica: As suas chaves/senhas são fortes? • Implementacional: Existem bugs no código? • Teórica dos jogos: Os incentivos estão alinhados para que trapacear não compense? Esse último é crucial, mas muitas vezes ignorado.

A segurança teórica dos jogos é sobre garantir que até mesmo atores racionais e egoístas prefiram seguir as regras - porque desviar-se custa mais do que ganha. É a "economia" da segurança.

CheckMate prova formal e automaticamente a segurança teórica dos jogos usando solucionadores SMT. O artigo introduz um algoritmo composicional de "dividir para conquistar" que escala para milhões de nós, intercalando geração de modelos e análise para eficiência.

Por que isso é importante: Agora podemos provar automaticamente, formalmente e em grande escala que os incentivos de um protocolo de blockchain tornam a trapaça irracional - antes da implementação.