Интересная статья прилетела от @makazone. Чувак из конторы eSpark рассказывает, как они использовали тул TLA+, чтобы найти баги в системе и оптимизировать узкие места. Суть инструмента в том, что на специальном языке (языке программирования, в некотором смысле) описывается система и то, в каких состояниях она должна быть, затем TLA+ гоняет эту модель всеми возможными способами и находит ошибки. Подробности, как всегда, найдешь по ссылке.

#modeling #testing #tool
https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f