10 июля 2026 года InfoQ выпустил подкаст о том, почему формальные методы наконец перестают быть игрушкой для узких специалистов. Если раньше разговор о спецификациях на TLA+ быстро заканчивался нервным смехом команды, то теперь ИИ, похоже, снимает главный барьер: помогает начать без нескольких недель погружения в новую математику и инструменты.
В беседе с ведущим Shane Hastie исследовательница и инженер Gabriela Moreira, которая сейчас возглавляет развитие Quint, объяснила, почему формальные методы стоит обсуждать не только в академической среде, но и в обычных продуктовых и инфраструктурных командах, сообщает InfoQ. Ключевая мысль простая: проблема никуда не делась, просто теперь появился более дешевый вход. Сложные распределенные системы, событийная архитектура, гонки, порядок событий, редкие состояния, которые почти невозможно удержать в голове, все это по-прежнему ломает прод. Разница в том, что в 2026 году инженер уже может не начинать с чистого листа.
Moreira давно работает над тем, чтобы сделать этот подход понятнее для практикующих разработчиков. Она пришла в тему через компиляторы и системы типов, занималась Haskell и инструментами для TLA+, а затем продолжила эту линию уже в индустрии. По ее словам, около восьми лет она пытается упростить вход в formal methods, а последние четыре года строит Quint в компании Informal Systems. Quint она описывает как более доступный язык спецификаций, основанный на идеях TLA+, но без части порога, который отпугивал новичков. Сейчас проект выделяют в отдельную инициативу, а сама Moreira за последний месяц перешла из роли ведущего разработчика в CEO спин-аута Quint.
Самое интересное в этом разговоре не новый язык как таковой, а новая роль ИИ вокруг него. Moreira прямо говорит: если вы инженер и уперлись в систему, где важен порядок событий, начните с того, что попросите любимый ИИ написать для вас спецификацию на Quint или TLA+. Не ради красивого текста, а ради исполнимой модели. Дальше ее нужно прогонять: запускать model checking, смотреть возможные поведения, проверять, можно ли прийти в нежелательное состояние, искать сценарии, которые команда не продумала в коде и тестах. И здесь ИИ полезен не как оракул истины, а как ускоритель старта. Он помогает описать машину состояний, а затем инженер уже проверяет, что именно эта машина говорит о системе.
В этом месте Moreira аккуратно разводит спецификации и обычное тестирование. Хорошие тесты по-прежнему нужны, но тест обычно проверяет набор ожидаемых сценариев, которые кто-то уже придумал. Формальная спецификация описывает пространство допустимого поведения системы и свойства, которые должны сохраняться при любом ходе событий. Для распределенных систем это важная разница. Если у вас сервис зависит от очередности сообщений, блокировок, повторных доставок или конкурентных операций, то список ручных тест-кейсов быстро превращается в игру на удачу. Спецификация и модель позволяют не гадать, а системно перебирать состояния. А потом поверх этого уже можно строить model-based testing, то есть буквально проигрывать смоделированные сценарии на реальной реализации и ловить расхождения между тем, что система должна делать, и тем, что она делает на самом деле.
Еще один исторический тормоз Moreira называет без дипломатии: слишком много скучного клея между моделью и кодом. Даже если команда соглашалась, что формальная модель полезна, дальше начиналась проза жизни. Нужно было связать описание поведения с реальным приложением, подготовить интерфейсы, написать техническую обвязку для повторного воспроизведения сценариев. Это не та работа, на которой хочется тратить лучшие часы сильного инженера. По мнению Moreira, именно здесь ИИ в 2026 году бьет особенно метко: он заметно упрощает генерацию такого glue code и тем самым делает model-based testing из красивой идеи более реалистичной инженерной практикой.
Для русскоязычной IT-аудитории здесь важен не только академический сюжет, но и очень приземленный управленческий вывод. Если вход в формальные методы действительно снижается, меняется сама экономика качества. Технологическим директорам это дает шанс раньше находить ошибки в критичных сценариях, а не после инцидента. Продуктовым командам это дает более точный способ обсуждать, что система вообще обязана делать в пограничных случаях. Для senior-разработчиков это шанс вынести спор о корректности из чатов и созвонов в исполнимую модель. А для HR и фаундеров здесь полезный сигнал другого рода: рынок постепенно будет ценить не только умение “быстро накидать фичу”, но и способность формализовать поведение сложных систем так, чтобы его можно было проверить машиной.
При этом Moreira не продает сказку о том, что ИИ заменит инженера. Наоборот, ее главный тезис почти антимаркетинговый: определить, какое поведение системы считать правильным, а какое неправильным, остается человеческой работой. Модель можно сгенерировать. Обвязку можно сгенерировать. Даже часть тестов можно сгенерировать. Но решение о том, что для бизнеса, пользователя и архитектуры считается корректным состоянием, все еще принимает человек. И это, пожалуй, самый здравый вывод из всей дискуссии. Если ИИ и правда делает формальные методы массовее, то главным дефицитом станет не синтаксис TLA+ или Quint, а способность команды внятно сформулировать собственные инварианты до того, как за нее это сделает продакшен через очередной сбой.