На прошлой неделе на OOPSALA '25 наши разработчики Act представили улучшенную, масштабируемую версию CheckMate, автоматического доказателя для формальной проверки теоретической безопасности блокчейн-протоколов. Короче говоря: инструмент проверяет, делают ли стимулы в протоколе мошенничество невыгодным.

Протоколы нуждаются в 3 видах безопасности: • Криптографическая: Ваши ключи/пароли надежны? • Реализация: Есть ли ошибки в коде? • Игровая теория: Соответствуют ли стимулы так, чтобы обман не приносил выгоды? Последний пункт имеет решающее значение, но часто игнорируется.

Игровая теория безопасности заключается в том, чтобы убедиться, что даже рациональные, эгоистичные участники предпочитают следовать правилам — потому что отклонение от них стоит больше, чем приносит. Это "экономика" безопасности.

CheckMate формально и автоматически доказывает безопасность в теории игр с использованием SMT-решателей. В статье представлен композиционный алгоритм "разделяй и властвуй", который масштабируется до миллионов узлов, чередуя генерацию моделей и анализ для повышения эффективности.

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