Формальная верификация

Модельное проверение заключается в систематическом и полном исследовании математической модели системы. Такой анализ возможен для конечных моделей, а также для некоторых видов бесконечных моделей, если удаётся эффективно задать бесконечные множества состояний путём абстрагирования или использования симметрии. Обычно процедура сводится к перебору всех состояний и переходов в модели, где для ускорения расчётов применяют специальные предметно-ориентированные методы абстрагирования, позволяющие рассматривать целые группы состояний единой операцией. К числу техник реализации относятся: перебор пространства состояний, символьный перебор пространства состояний, абстрактная интерпретация, символическое моделирование, уточнение абстракций. Свойства, подлежащие проверке, часто описываются при помощи темпоральных логик, например, линейная темпоральная логика (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA)^[7], или компьютерная древовидная логика (CTL). Главным преимуществом модельного проверения считается высокая степень автоматизации; основной недостаток — трудности масштабирования на крупные системы: символьные модели обычно ограничиваются несколькими сотнями бит состояния, тогда как явный перебор требует сравнительно небольшого размера пространства состояний. Для повышения масштабируемости алгоритма IC3/PDR при использовании SAT-солверов применяются такие современные методы, как:

• Decide and Propagate in Domain — сокращение числа переменных, по которым принимаются решения. Перед каждым этапом решения вычисляется ограниченное подмножество релевантных переменных, что существенно уменьшает нагрузку на SAT-солвер при распространении ограничений^[8].
• VSIDS by Bucket — замена традиционной бинарной кучи на систему корзин для эвристики VSIDS. Это позволяет выполнять операции добавления и извлечения переменных за константное время вместо логарифмического, снижая накладные расходы на поддержание их порядка^[8].
• Without Resetting — поддержка временных клауз с переиспользованием одной активационной переменной. Метод позволяет удалять временные клаузы и производные от них выученные правила после каждого запроса без полного сброса SAT-солвера, сохраняя накопленные эвристические оценки^[8].

Другим подходом является дедуктивная верификация^[9][10]. Она включает в себя построение по системе и её спецификации (а иногда и по дополнительным аннотациям) набора математических «обязательств к доказательству» (proof obligations), истинность которых гарантирует соответствие системы спецификации, а затем — доказательство этих обязательств с помощью помощников доказательств (интерактивных проверяющих теорем), таких как HOL, ACL2, Isabelle, The Rocq Prover (версия 9.2.0, ранее известный как Coq), Lean 4 (применяемый для математики и функционального программирования)^[11], PVS, либо при помощи автоматических доказателей теорем, в частности решателей задачи выполнимости по теориям (SMT). Недостатком этого способа является то, что от пользователя может потребоваться глубокое понимание причин корректности системы и уточнение этой информации для инструмента проверки — в виде последовательности теорем для доказательства или посредством формализации спецификаций (инвариантов, предусловий, постусловий) для компонентов и, возможно, их подкомпонентов.

Формальная верификация программ заключается в доказательстве того, что программа удовлетворяет формальной спецификации её поведения. К направлениям формальной верификации относятся дедуктивная верификация, абстрактная интерпретация, автоматическое доказательство теорем, типовые системы, а также облегчённые формальные методы. Одним из перспективных подходов, основанных на типах, выступает программирование с зависимыми типами, при котором типы функций (частично или полностью) включают формальные спецификации, а успешная проверка типов эквивалентна доказательству корректности реализованного кода относительно спецификаций. Полноценные языки с поддержкой зависимых типов позволяют воспринимать дедуктивную верификацию как частный случай проверки типов.

Другим дополнительным подходом является выведение программ, когда эффективный код строится по функциональной спецификации через последовательность преобразований, сохраняющих корректность. Примером такого подхода служит формализм Бёрд—Мертенс, рассматриваемый также как одна из форм синтеза программ. В 2026 году активно развивается «верикодинг» — генерация кода с доказанной корректностью на основе формальных спецификаций с помощью больших языковых моделей (LLM) (проекты ATLAS, DafnyPro, MiniF2F-Dafny)^[12].

Перечисленные методы могут быть «корректными», то есть гарантировать логическое следование свойств программы из её семантики, или «некорректными», когда такой гарантии нет. Корректная методика возвращает результат только после анализа всего пространства возможностей; пример некорректной — покрывающей лишь их подмножество, например, только целые числа в определённом диапазоне, чаще всего выносящей «достаточно хороший» ответ. Техники могут также быть «разрешимыми» — их алгоритмы гарантированно завершаются выдачей результата, или неразрешимыми, когда вычисления теоретически могут идти бесконечно. При ограничении области рассмотрения возможна реализация некорректной, но разрешимой методики, если корректная разрешимость недостижима.

Рост сложности проектируемых систем делает формальные методы анализа всё более востребованными в аппаратной сфере^[14][15]. В настоящее время формальная верификация используется большинством ведущих производителей аппаратного обеспечения^[16], тогда как в разработке программного обеспечения распространение этих методов остаётся низким. Это объясняется большей востребованностью формальных методов именно в аппаратной сфере, где ошибки часто приводят к ощутимым экономическим потерям. Кроме того, из-за возможности сложных взаимодействий между компонентами становится всё труднее охватить все сценарии поведения исключительно методом симуляции, тогда как многие задачи аппаратного проектирования формализуемы и поддаются автоматическим доказательствам, благодаря чему внедрение формальной верификации для аппаратных решений проще и эффективнее^[17].

По состоянию на 2011 год были формально верифицированы несколько операционных систем: Secure Embedded L4 microkernel, созданный NICTA (и реализуемый коммерчески как seL4 компанией OK Labs)^[18], ОС реального времени ORIENTAIS, созданная на базе OSEK/VDX в Восточно-Китайском педагогическом университете, Integrity от Green Hills Software, а также PikeOS от SYSGO^[19][20]. В 2016 году команда под руководством Чжуна Шао в Йельском университете разработала формально верифицированный микроядро CertiKOS^[21][22]. В 2026 году была успешно завершена формальная верификация безопасности микроядра seL4 для архитектуры AArch64 с математическим доказательством его конфиденциальности, изоляции и функциональной корректности^[23].^[24][25].

По состоянию на 2017 год формальная верификация применяется при проектировании масштабных компьютерных сетей на основе строгого математического моделирования^[26], а также в рамках нового класса технологий — сетей на основе намерений^[27]. Крупные разработчики сетевого ПО, предлагающие решения формальной верификации, включают Cisco^[28], Forward Networks и Veriflow Systems.

Язык программирования SPARK содержит инструменты, позволяющие вести разработку с формальной верификацией, и используется в ряде ответственных промышленных систем. Компилятор CompCert реализует большую часть стандарта ISO C и формально верифицирован как корректный^[29][30].

Формальные методы активно применяются крупными облачными провайдерами для обеспечения безопасности и корректности работы инфраструктуры. В Amazon Web Services (AWS) используются инструменты Zelkova для анализа политик доступа (включая IAM Access Analyzer и проверку политик S3) и Tiros для проверки сетевой инфраструктуры и достижимости ресурсов^[31][32]. Для верификации алгоритмов в таких сервисах, как Amazon S3, DynamoDB и Amazon EBS, AWS применяет языки спецификаций TLA+ и PlusCal^[33]. В свою очередь, Microsoft использует автоматическое средство доказательства теорем Z3 для проверки глобальных свойств сетей центров обработки данных в облаке Microsoft Azure^[32].

Для формальной верификации смарт-контрактов в сетях Ethereum и Solana применяется ряд специализированных инструментов. Certora Prover используется для автоматической верификации контрактов, при этом формальные спецификации задаются на специализированном языке CVL (Certora Verification Language). Для смарт-контрактов на языке Solidity применяются встроенный в компилятор инструмент Solidity SMTChecker, который статически проверяет исходный код во время компиляции, и solc-verify — расширенная версия компилятора, позволяющая интегрировать спецификации (инварианты, пред- и постусловия) непосредственно в код в виде аннотаций^[34][35][36].

Интеграция систем искусственного интеллекта с языком формальной верификации Lean применяется для автоматизации математических доказательств. В частности, система AlphaProof в связке с Lean успешно использовалась для решения сложных задач Международной математической олимпиады, а в начале 2026 года с помощью ИИ и Lean была решена проблема Эрдёша 1196, остававшаяся открытой 60 лет. Использование языка формальной логики позволяет автоматически проверять сгенерированные доказательства, что надёжно исключает проблему нейросетевых галлюцинаций.