Разрабатывать конкурентные системы сложно. Самые плохие ошибки закрадываются в алгоритм еще на стадии проектирования, не находятся никакими тестами и ждут реальной нагрузки и своей уникальной последовательности событий, чтобы взорваться и всё испортить.

Находить такие ошибки можно, даже не написав ни строчки кода — если пользоваться методами формальной верификации алгоритмов. Таких методов много, но один из них — разработанный в 1999 г. Лесли Лампортом (Leslie Lamport) формализм TLA+ и инструмент верификации TLC — оказался ближе всего инженерам и приобретает все большую популярность.

Мы поговорим про TLA+/TLC, про PlusCal — транслируемый в TLA+ язык спецификации алгоритмов специально для инженеров, про инструментарий, а также про практики применения TLA+/TLC в реальных проектах.