Команда Specula протестировала возможности современных больших языковых моделей в задаче формальной верификации кода, используя язык спецификаций TLA+. Эксперты оценили работу таких систем на примере реализации алгоритма Raft в проекте Etcd. Результат оказался удивительным: модели вроде Claude часто генерируют код, который проходит базовую проверку синтаксиса и запускается в инструменте TLC, но он описывает стандартные теоретические шаблоны, а не реальные детали конкретной системы. Исследователи заметили, что AI просто переписывает данные из научных статей, вместо того чтобы абстрагировать логику из сложного исходного кода.
Для выявления таких проблем создана бенчмарка SysMoBench, которая предоставляет моделям данные по eleven системам, охватывающим как синхронизацию, так и распределенные протоколы. Оценка проходит в четыре этапа: проверка синтаксиса, запуск симуляции, проверка соответствия коду и верификация инвариантов. Первые два этапа показывают высокие баллы, но уже на третьем этапе обнаруживаются системные ошибки. Модели генерируют состояния, в которые реальная система никогда не зайдет, или пропускают важные переходы. Например, Claude incorrectly накапливает все голоса в наборе, игнорируя перезапись старых значений, что приводит к несовпадению с семантикой ZooKeeper. В других случаях модель сливает многошаговые операции в одну атомарную проверку, блокируя нормальные переходы процесса.
Итоговые цифры разительно отличаются от ожиданий. Хотя синтаксическая верификация проходит почти на 100%, баллы соответствия реальному коду на сложных распределенных системах падают до 25%, а инвариантов — до 16%. Новые модели вроде Gemini 3.1 показывают лучшие результаты, но проблема остается. Команда выявила три главных препятствия для автоматизации. Во-первых, метод проверки через переходы зависит от выборки трассировки, поэтому не покрытые пути в коде остаются без внимания. Во-вторых, абстракция состояний неизбежно теряет информацию о содержании переменных, и исправить это приходится вручную. В-третьих, добавление новой системы требует написания специальных шаблонов и подсистем, пока полная автоматизация недоступна.
Несмотря на трудности, команда работает над агентом Specula, который уже добился идеальных результатов на текущих задачах. Этот специализированный инструмент способен самостоятельно читать репозитории, решать, что моделировать, и проводить полный цикл спецификации. Лидерборд проекта продолжает расширяться новыми моделями и системами. Исследователи приглашают сообщество к сотрудничеству, так как полностью решить поставленные проблемы одной автоматизацией пока не удалось.