Воркшоп: TLA+/TLC: практичный инструмент формальной верификаций алгоритмов