Minulý týden na konferenci OOPSALA '25 představili naši vývojáři Act vylepšenou, škálovatelnou verzi CheckMate, automatizovaného dokazovače pro formální ověření bezpečnosti blockchainových protokolů z hlediska teorie her. Stručně řečeno: nástroj kontroluje, zda pobídky v protokolu nestojí za to.

Protokoly potřebují 3 druhy zabezpečení: • Kryptografické: Jsou vaše klíče/hesla silná? • Implementační: Jsou v kódu chyby? • Teorie her: Jsou pobídky sladěny tak, aby se podvádění nevyplácelo? To poslední je zásadní, ale často se ignoruje.

Bezpečnost založená na teorii her spočívá v tom, že se ujistíme, že i racionální, sobečtí aktéři dávají přednost dodržování pravidel - protože odchýlení stojí více, než vydělává. Je to "ekonomika" bezpečnosti.

CheckMate formálně a automaticky prokazuje bezpečnost z teorie her pomocí SMT řešičů. Článek představuje kompoziční algoritmus "rozděl a panuj", který se škáluje na miliony uzlů a prokládá generování a analýzu modelu pro zvýšení efektivity.

Proč je to důležité: Nyní můžeme automaticky, formálně a ve velkém měřítku dokázat, že pobídky blockchainového protokolu činí podvádění iracionálním – ještě před nasazením.