Минулого тижня на OOPSALA '25 розробники нашого Act представили покращену, масштабовану версію CheckMate, автоматизованого засобу для офіційної перевірки теоретичної безпеки протоколів блокчейну. Якщо коротко: інструмент перевіряє, чи не роблять стимули в протоколі обманом того не варто.

Протоколи потребують 3 видів безпеки: • Криптографічні: чи надійні ваші ключі/паролі? • Імплементація: Чи є помилки в коді? • Теоретика гри: Чи узгоджені стимули так, що шахрайство не окупається? Останнє є критично важливим, але часто ігнорується.

Теоретико-ігрова безпека полягає в тому, щоб переконатися, що навіть раціональні, егоїстичні актори вважають за краще дотримуватися правил, тому що відхилення коштує більше, ніж заробляє. Це «економіка» безпеки.

CheckMate формально та автоматично доводить безпеку теоретики гри за допомогою SMT розв'язувачів. У статті представлено композиційний алгоритм «розділяй і володарюй», який масштабується до мільйонів вузлів, перемежовуючи генерацію та аналіз моделей для ефективності.

Чому це важливо: Тепер ми можемо автоматично, формально та масштабно довести, що стимули протоколу блокчейну роблять шахрайство нераціональним - до розгортання.