TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов (ITooLabs).