Forrige uke på OOPSALA '25 presenterte våre Act-utviklere en forbedret, skalerbar versjon av CheckMate, en automatisert beviser for å formelt verifisere den spillteoretiske sikkerheten til blokkjedeprotokoller. Kort sagt: verktøyet sjekker om insentivene i en protokoll gjør juks ikke verdt det.

Protokoller trenger 3 typer sikkerhet: • Kryptografisk: Er nøklene/passordene dine sterke? • Implementering: Er det feil i koden? • Spillteoretisk: Er insentivene tilpasset slik at juks ikke lønner seg? Den siste er avgjørende, men ofte ignorert.

Spillteoretisk sikkerhet handler om å sørge for at selv rasjonelle, egoistiske aktører foretrekker å følge reglene – fordi avvik koster mer enn det tjener. Det er «økonomien» i sikkerhet.

CheckMate beviser formelt og automatisk spillteoretisk sikkerhet ved hjelp av SMT-løsere. Artikkelen introduserer en komposisjonell "splitt-og-hersk"-algoritme som skaleres til millioner av noder, og fletter sammen modellgenerering og analyse for effektivitet.

Hvorfor dette er viktig: Vi kan nå automatisk, formelt og i stor skala bevise at en blokkjedeprotokolls insentiver gjør juks irrasjonelt - før distribusjon.