Afgelopen week op OOPSALA '25 hebben onze Act-ontwikkelaars een verbeterde, schaalbare versie van CheckMate gepresenteerd, een geautomatiseerde prover voor het formeel verifiëren van de speltheoretische beveiliging van blockchainprotocollen. Kortom: de tool controleert of de prikkels in een protocol het niet waard maken om te valsspelen.

Protocollen hebben 3 soorten beveiliging nodig: • Cryptografisch: Zijn je sleutels/wachtwoorden sterk? • Implementatie: Zijn er bugs in de code? • Speltheoretisch: Zijn de prikkels zo afgestemd dat vals spelen niet loont? Die laatste is cruciaal, maar wordt vaak genegeerd.

Speltheoretische beveiliging gaat erom ervoor te zorgen dat zelfs rationele, egoïstische actoren de voorkeur geven aan het volgen van de regels - omdat afwijken meer kost dan het oplevert. Het is de "economie" van beveiliging.

CheckMate bewijst formeel en automatisch game-theoretische veiligheid met behulp van SMT-oplossers. Het paper introduceert een compositie "divide-and-conquer" algoritme dat schaalt naar miljoenen knooppunten, waarbij modelgeneratie en analyse voor efficiëntie worden afgewisseld.

Waarom dit belangrijk is: We kunnen nu automatisch, formeel en op grote schaal bewijzen dat de prikkels van een blockchainprotocol het bedrog irrationeel maken - vóór de implementatie.