Игорь Коннов. Apalache: symbolic model checker for TLA+

TLA+ -- формальный язык, предназначенный для спецификации всех видов компьютерных систем. Системные архитекторы применяют TLA+ для описания параллельных, распределенных и отказоустойчивых протоколов. Такие системы обычно описываются на полуформальных языках в виде псевдокода или диаграмм состояний. Мы применяем TLA+ для описания протоколов в экосистеме блокчейнов Tendermint/Cosmos. В первой половине доклада мы рассмотрим принципы спецификации протоколов на примере протокола обмена криптотокенами в системе Cosmos IBC. На основе примера показывается подход к итеративной разработке протоколов с применением верификатора моделей Apalache. Во второй половине доклада мы рассмотрим принципы работы Apalache. Apalache транслирует спецификацию на языке TLA+ в систему логических ограничений на языке SMTLIB и вызывает решатель Z3 для проверки ограничений..