La scorsa settimana a OOPSALA '25, i nostri sviluppatori Act hanno presentato una versione migliorata e scalabile di CheckMate, un provatore automatico per verificare formalmente la sicurezza teorica dei giochi dei protocolli blockchain. In breve: lo strumento verifica se gli incentivi in un protocollo rendono la frode non conveniente.

I protocolli necessitano di 3 tipi di sicurezza: • Criptografica: Le tue chiavi/password sono forti? • Implementativa: Ci sono bug nel codice? • Teorica dei giochi: Gli incentivi sono allineati in modo che imbrogliare non convenga? Quest'ultimo è cruciale, ma spesso ignorato.

La sicurezza teorica dei giochi riguarda l'assicurarsi che anche attori razionali e egoisti preferiscano seguire le regole - perché deviare costa più di quanto guadagni. È l'"economia" della sicurezza.

CheckMate dimostra formalmente e automaticamente la sicurezza teorica dei giochi utilizzando risolutori SMT. Il documento introduce un algoritmo compositivo di "divide et impera" che scala a milioni di nodi, intercalando generazione di modelli e analisi per efficienza.

Perché questo è importante: Ora possiamo dimostrare automaticamente, formalmente e su larga scala che gli incentivi di un protocollo blockchain rendono irrazionale imbrogliare - prima del deployment.