Немного трезвости в разговорах о формальной верификации
На прошлой неделе Борис Чёрни, создатель Claude Code, упомянул, что Opus смог использовать TLA+ для обнаружения race conditions в коде.
И теперь весь интернет обсуждает формальную верификацию.
Для давнего сторонника и педагога TLA+ это действительно волнующе. TLA+ отлично подходит для проектирования сложных распределённых систем и убеждения в том, что они работают без ошибок. Но одновременно, как сторонник рассудительности, эта новая эйфория настораживает. Можно услышать множество утверждений о том, что формальные методы разрешат проблему разработки агентного ПО раз и навсегда — это полная чушь.
Уже много написано о слабостях TLA+ в том, что он не может гарантировать, например, что корректные спецификации автоматически переводятся в корректный код. Но хочется сосредоточиться на другом ограничении: чтобы проверить свойство, нужно сначала иметь возможность его выразить. Какие же свойства TLA+ просто не может выразить?
(Предполагается базовое знакомство с TLA+. Если вы совсем новичок, посмотрите материалы или прочитайте введение.)
Что TLA+ может проверять
TLA+ разделяет систему на набор поведений. Каждое поведение — это последовательность состояний, например "первый светофор горит зелёным, потом жёлтым, потом красным". В каждом состоянии можно выражать обычные булевы выражения вроде "светофор четыре горит зелёным" или "все светофоры красные". Кроме того, используются три "временные" логические оператора:
[]P("всегда P") — истинно, если P истинно в текущем состоянии и во всех будущих состояниях. Пример:[](at_most_one_green)истинно, если в любом будущем состоянии горит не больше одного зелёного света.P'("P штрих") — истинно, если P истинно в следующем состоянии. Пример:light="green" && light'="red"истинно, если свет переходит из зелёного в красный.<>P("в конце концов P") — истинно, если P истинно в текущем состоянии или в хотя бы одном будущем состоянии. Пример:<>(light4 = "yellow")истинно, если свет четыре жёлтый или станет жёлтым в будущем.
Когда говорят, что P — свойство системы, имеют в виду, что P истинно в начальном состоянии каждого поведения. Если проверяют свойство []P, это значит, что []P истинно в каждом начальном состоянии, и по определению "всегда" P истинно в любом будущем состоянии из этого начального состояния, то есть в каждом состоянии каждого поведения. Это называют инвариантом — одно из самых фундаментальных свойств, проверяемых в TLA+.
Можно также комбинировать [] с штрихами, получая свойства действий, или вариант-свойства. [](x' >= x) истинно, если новое значение x всегда больше или равно старому значению x. Другой забавный пример — [](P => P'): как только P становится истинным, оно не может снова стать ложным. Настоящий TLA+ сложнее из-за чего-то под названием "stutter-invariance", но это детали. Свойства действий и инварианты — это оба safety-свойства, что примерно означает "что-то плохое никогда не произойдёт". О safety и liveness есть отдельная статья.
Liveness, кстати, — это "что-то хорошее всегда происходит". Все liveness-свойства основаны на <>. Сам по себе <>P означает просто "P истинно в хотя бы одном состоянии каждого поведения", что обычно слишком слабо для нормального системного свойства. Но с комбинированием получаются интересные liveness-свойства:
[]<>Pистинно, если в каждом состоянии P истинно в хотя бы одном будущем состоянии. Это представляет механизмы восстановления, типа "Если узлы проводят переизбрание лидера, они в конце концов согласуют нового лидера".<>[]Pистинно, если в какой-то момент времени P становится истинным и остаётся истинным навсегда. Это хорошо для показа завершения алгоритмов с правильным результатом.[](P => <>Q)истинно, если для любого состояния, где P истинно, существует будущее состояние, где Q истинно. Это может показать, что P в конце концов вызывает Q, или что "все сообщения в очереди в конце концов попадают в историю читателя". Парсить формулу немного сложно, поэтому используют сахарP ~> Q(P ведёт к Q).
Есть несколько других операторов, типа ENABLED и <<A>>_v, открывающих другие возможности, но большинство проверяемого — это инварианты, свойства действий и liveness. И уточнение, которое комбинирует safety и liveness и представляет отдельную тему.
Что TLA+ не может делать
Начнём с очевидного: если неизвестно, как выразить свойство логической формулой, TLA+ не поможет. И никакой формальный метод не поможет. Если невозможно формализовать человеческое понимание птицы, нельзя доказать, что приложение правильно их распознаёт. К сожалению, множество важных свойств, о которых думают, попадают в эту категорию.
Дальше — слишком специфичные вещи. Safety-свойства TLA+ работают на уровне либо отдельных состояний (инварианты), либо одного шага (свойства действий). Нельзя нативно определить свойство на два или больше шагов, например "нажатие delete и потом undo возвращает исходное состояние" или "после нажатия power компьютер включается в течение десяти шагов". Также нельзя определять свойства на операциях с плавающей точкой или реальном времени, только логическом времени.
Теперь ограничение, которое интересует больше всего. Свойства TLA+ неявно квантифицированы по всем поведениям. Сказано, что проверка []P означает "P истинно в каждом состоянии", но на самом деле означает "для всех поведений []P истинно в начальном состоянии этого поведения". Любое свойство, которое TLA+ может проверить систему, должно быть свойством, истинным для каждого отдельного поведения.
Что это исключает? Намного больше, чем можно ожидать!
Во-первых, невозможно сказать "существует поведение, где P истинно". Нельзя сказать, что P возможно, даже если на него напрямую не попадаем. Пример — доказать, что игра выигрываема. Это называют свойствами достижимости. Более продвинутые свойства достижимости — вроде "P достижимо из каждого начального состояния" или "P достижимо из любого состояния, где истинно Q".
Также невозможно определять свойства над набором поведений. Это называют гипер-свойством. Скажем, моделируем аппаратное обеспечение телефона и хотим проверить, что режим экономии энергии всегда использует меньше энергии, чем обычный режим. Свойство: "любая последовательность действий использует не больше энергии в режиме экономии, чем в обычном режиме". Чтобы это опровергнуть, нужны два поведения, одинаковые кроме того, что одно начинается в режиме экономии, другое нет, и обычный режим использует меньше энергии. Одного поведения недостаточно, так что это невозможно проверить нативно в TLA+.
Гипер-свойства могут казаться нишевыми, но они покрывают множество security-свойств и все статистические свойства ("95%-й перцентиль времени отклика — 5ms").
Наконец, немного более академично, невозможно определять свойства над пространством состояний в целом. Нельзя сказать, например, что существует только один путь из состояния X в Y. Неизвестно, насколько это было бы полезно на практике. Большинство таких "метасвойств" выглядят потенциально значимыми, просто конкретных примеров не видно.
То, что TLA+ "может" "делать"
Когда сказано, что TLA+ не может этого делать, несколько упрощено. Имеется в виду: если пишется спецификация, и она напрямую соответствует строящейся системе, то TLA+ не может выражать эти свойства как свойства системы. Но можно имитировать двухшаговые свойства вспомогательными переменными, например, сохраняя все изменения состояния в последовательности state_history и определяя свойство как инвариант этой последовательности. Некоторые гипер-свойства можно имитировать самокомпозицией, где каждое поведение самокомпозированной спецификации — это два поведения реальной системы. Основной model checker TLA+ (TLC) может проверять самые базовые свойства достижимости с новым ключевым словом REACHABLE и некоторые свойства пространства состояний с помощью TLCGet. Эндрю Хелвер написал безумно остроумный пост об имитации "всегда достижимо" с помощью fairness и "machine closure".
Это полезные трюки, но остаются хаками. Каждый требует много остроумия и сопровождается серьёзными недостатками. Вспомогательные переменные портят уточнения, самокомпозиция экспоненциально увеличивает пространство состояний и так далее. Хаки плохо комбинируются с другими возможностями TLA+ и не покрывают все тонкости свойств, которые захочется выразить. И хуже всего, они делают модели странными и грязными и не соответствующими реальным системам.
Можно также использовать другой инструмент с другим фокусом. CTL может проверять свойства достижимости, PRISM — вероятностные свойства и так далее. Они жертвуют тем, в чём TLA+ хорош, и конечно ни один не решает проблему свойств, которые нельзя выразить логически.
В итоге TLA+ довольно хорош в сборке множества низко висящих плодов — инварианты и liveness покрывают многое, что заботит, и TLA+ разумно хорош в их выражении и проверке. Есть большой потенциал (и много ловушек) в использовании TLA+ для проверки кода, написанного "на чувство". Но также множество вещей, которые он вообще не может выразить, не то что проверить.