Что такое формальные методы

Формальные методы — это математически строгие техники для спецификации, проектирования и верификации программных и аппаратных систем. Вместо тестирования отдельных сценариев формальные методы позволяют доказать свойства системы для всех возможных состояний и путей исполнения.

Ключевая идея: система описывается на языке с точной математической семантикой, после чего автоматические инструменты (model checkers, theorem provers, SAT/SMT-солверы) исчерпывающе проверяют заданные свойства — или находят контрпример (trace ошибки).

Откуда выросли

Формальные методы выросли из кризиса ПО 1960–70-х, когда стало ясно, что тестированием нельзя доказать отсутствие ошибок.

• Эдсгер Дейкстра (1968) — статья «Go To Statement Considered Harmful» и концепция структурного программирования. Позже — формализм weakest preconditions и книга «A Discipline of Programming» (1976), заложившие основу верификации программ.
• Тони Хоар (1969) — логика Хоара (Hoare logic): формальная система для рассуждения о корректности программ через пред- и постусловия {P} C {Q}. Фундамент для всех последующих верификационных подходов.
• Амир Пнуэли (1977) — применил темпоральную логику (temporal logic) к верификации реактивных систем. За это получил премию Тьюринга (1996). Темпоральная логика стала основой model checking.
• Эдмунд Кларк, Аллен Эмерсон, Жозеф Сифакис (1981–82) — независимо друг от друга изобрели model checking — автоматическую проверку конечных моделей систем против темпоральных свойств. Тьюринговская премия 2007.
• Лесли Лэмпорт — создатель TLA+ (Temporal Logic of Actions, 1999). Формализм для спецификации конкурентных и распределённых систем. Лэмпорт — также автор алгоритмов Paxos, Bakery, Lamport clocks. Тьюринговская премия 2013.
• Робин Милнер — процессные алгебры (CCS, π-calculus) для моделирования конкурентных систем. Тьюринговская премия 1991.

Зачем нужны

Тестирование проверяет отдельные сценарии. Формальная верификация проверяет все возможные сценарии.

Формальные методы особенно ценны для:

• Конкурентных и распределённых систем, где количество состояний комбинаторно взрывается
• Протоколов, где нужно гарантировать safety (ничего плохого не происходит) и liveness (что-то хорошее рано или поздно происходит)
• Критических систем, где цена бага — деньги, репутация или жизни

Конкретные примеры применения, результаты и уроки — в разделе Формальные методы в индустрии.

Ландшафт инструментов

Классические инструменты

TLA+

Статус: активная разработка, новая организационная структура

• Создан TLA+ Foundation, который финансирует разработку и выпускает ежемесячные отчёты
• VS Code расширение активно развивается и заменяет устаревший Eclipse Toolbox — добавлена поддержка Model Context Protocol, визуализация статистик симуляции TLC
• Экосистема: 3 парсера (SANY, TLAPM, tree-sitter), 3 model checker-а (TLC, Apalache, Spectacle), proof manager (TLAPM)
• Проблемы: 25-летний Java-кодбаз, мало тестов, уход оригинальных разработчиков. Обсуждается bytecode-интерпретатор с потенциальным ускорением в 1000x
• Совместный с NVIDIA GenAI-Accelerated TLA+ Challenge — исследование применения LLM для генерации спецификаций

Подробный обзор: The current state of TLA+ development (May 2025)

Alloy

Статус: стабильный, Alloy 6.2.0 (январь 2025)

• Alloy 6 — крупная ревизия: мутабельное состояние, темпоральная логика, новые солверы, улучшенный визуализатор
• Вышла книга Practical Alloy — hands-on guide по Alloy 6+
• Сильные стороны: SAT-based анализ (быстро), отличная работа с графами и отношениями, transitive closure
• Слабее TLA+ по выразительности, но проще для структурного моделирования

SPIN / Promela

Статус: зрелый, поддерживается

• SPIN — классический model checker для конкурентных протоколов (LTL, Büchi автоматы)
• Генерирует проблемно-специфический model checker на C — быстрый и эффективный по памяти
• Сообщество стабильное, но без заметных новых фич в последние годы

Новые альтернативы

Quint

Статус: активная разработка, Informal Systems

• Quint — современный язык спецификаций на базе TLA (логики), но с программистским синтаксисом вместо LaTeX-нотации
• Типизация, режимы (pure/action/temporal), REPL, CLI, мгновенная обратная связь
• Использует Apalache как бэкенд для символической проверки
• Внимание: разработка Apalache замедлилась после выделения из Informal Systems в конце 2024

P (Microsoft Research)

Статус: зрелый, используется в продакшне

• P — язык на основе стейт-машин для моделирования асинхронных распределённых систем
• Ключевое отличие от TLA+: P-программы компилируются в исполняемый C-код — мост между моделью и реализацией
• Используется в AWS (анализ S3) и Microsoft (USB-драйверы Windows — найдено 300+ багов)

Stateright (Rust)

Статус: нишевый, но интересный

• Stateright — model checker встроенный прямо в Rust-код
• Верифицирует реализацию, а не отдельную модель — нет разрыва между спецификацией и кодом
• Включает linearizability tester (аналог Jepsen, но исчерпывающий)
• Быстрее TLC, особенно на больших state spaces

Dafny

Статус: активная разработка, Amazon

• Dafny — verification-aware язык программирования
• Amazon использует для Cedar (authorization policy language) — доказательство корректности валидатора
• Активное исследование по автоматизации доказательств с помощью LLM (VeriCoding benchmarks)

Verus (Rust)

Статус: активное академическое развитие

• Verus — формальная верификация Rust-кода
• Различает ghost types (для спецификаций) и нативные Rust типы
• Активное исследование: AutoVerus — автоматическая генерация proof-аннотаций через LLM
• Бенчмарки 2025–2026: 21k+ Rust-программ, 9700+ верифицированных

Lean 4

Статус: растущая экосистема

• Theorem prover и язык программирования одновременно
• Активно используется в математике (Mathlib) и начинает применяться для верификации ПО
• Включён в мульти-языковые бенчмарки вместе с Dafny и Verus

Сводная таблица

Тренды

• Сближение формальных методов с ИИ — генерация спецификаций и доказательств через LLM
• Стирание границы между моделью и реализацией — P, Stateright, Verus
• Lightweight formal methods — Amazon Cedar/Dafny, практические подходы к верификации в продакшне

Формальные методы в индустрии: кейсы и результаты

Формальные методы — не только академическая дисциплина. Ниже — конкретные случаи применения в индустрии с числами, результатами и уроками.

Успехи: где ФМ дали измеримый результат

Amazon Web Services — TLA+ и P

С 2011 года инженеры AWS используют TLA+ для верификации критических распределённых систем. По данным статьи Newcombe et al. (CACM, 2015), к моменту публикации 7 команд использовали TLA+ на 10 крупных реальных системах. Во всех случаях были найдены тонкие баги, которые не поймали ни code review, ни тестирование.

Конкретные результаты из статьи (Use of Formal Methods at Amazon Web Services):

Особенно показателен баг DynamoDB: кратчайший error trace содержал 35 высокоуровневых шагов. Баг прошёл через множественные design review, code review и месяцы тестирования, но был найден TLC model checker-ом за секунды.

Инженеры осваивали TLA+ за 2–3 недели и начинали получать полезные результаты.

К 2024–2025 году AWS расширила практики: помимо TLA+ теперь используется язык P (state-machine-based моделирование), property-based testing, fuzzing, deterministic simulation и runtime-валидация (Systems Correctness Practices at AWS, CACM 2024). Формальные спецификации используются как test oracle-ы — источник правильных ответов для всех остальных видов тестирования.

Intel — после катастрофы Pentium FDIV

В 1994 году в процессоре Pentium обнаружен баг в операции деления с плавающей точкой (FDIV bug). Причина: 5 из 1066 записей в lookup-таблице были пропущены из-за ошибки в скрипте генерации (Wikipedia: Pentium FDIV bug).

Стоимость отзыва: $475 миллионов (более $1 млрд в текущих ценах). IBM остановила отгрузки Pentium-компьютеров 12 декабря 1994 года, и через неделю Intel объявила полный отзыв (Ken Shirriff, 2024).

Последствия для Intel:

• Формальная верификация стала обязательной для арифметических модулей
• При разработке Pentium 4 использовались symbolic trajectory evaluation и theorem proving, предотвратившие аналогичные баги
• Архитектура Nehalem (2008) стала первой, где формальная верификация была основным методом валидации
• ~85 инженеров прошли обучение формальным методам

В целом по полупроводниковой индустрии верификация занимает 50–70% бюджета и сроков разработки чипа. Соотношение инженеров верификации к инженерам проектирования достигает 5:1 (Semiconductor Engineering).

Airbus — Astrée и CompCert

Astrée — статический анализатор на основе абстрактной интерпретации. Доказывает отсутствие runtime-ошибок (деление на ноль, переполнение, выход за массив) в C-программах.

Ключевой результат: в ноябре 2003 года Astrée полностью автоматически доказал отсутствие runtime-ошибок в ПО управления полётом (fly-by-wire) Airbus A340 (Astrée project):

• 132,000 строк C-кода проанализированы за 1 час 20 минут
• На PC с 2.8 GHz процессором, 300 MB памяти
• Ноль ложных срабатываний (zero false alarms)

С января 2004 года Astrée был расширен для анализа ПО электрического управления полётом A380, что было завершено до первого полёта A380 (27 апреля 2005).

CompCert — формально верифицированный компилятор C. Airbus использует CompCert для компиляции бортового ПО. Результат: улучшение worst-case execution time на 12% по сравнению с неверифицированными компиляторами (AbsInt CompCert).

В знаменитом исследовании Yang et al. (PLDI 2011) инструмент Csmith за 3 года нашёл 325+ ранее неизвестных багов в GCC, LLVM и других компиляторах. CompCert был единственным компилятором, в верифицированных частях которого Csmith не смог найти ошибок генерации неправильного кода.

DO-178C (2011) — обновлённый стандарт сертификации бортового ПО, впервые официально разрешающий использование формальной верификации вместо определённых видов тестирования (дополнение DO-333).

Парижское метро — линия 14 (Météor), B-метод

Линия 14 парижского метро — первая полностью автоматическая (беспилотная) линия метро в столице крупного государства. Открыта в 1998 году. Система автоматического управления поездами разработана Matra Transport International для RATP с использованием B-метода (CLEARSY).

Результаты:

• Разработка safety-critical ПО с использованием Atelier B (инструмент B-метода от CLEARSY)
• 27,800 лемм доказаны в ходе разработки; ~*90% доказаны автоматически*, оставшиеся 10% — интерактивно
• Код генерировался из B-спецификаций в Ada
• Ноль багов найдено после завершения доказательств — ни при функциональной валидации, ни при интеграционном тестировании, ни при испытаниях на месте, ни за всё время эксплуатации с 1998 года
• «Я никогда не видел ничего подобного: ПО было практически идеальным с первого раза» — Claude Hennebert, делегат RATP
• 25+ лет безотказной работы; интервал между поездами — до 85 секунд
• Ежедневный пассажиропоток вырос с 240,000 (2003) до 500,000+

B-метод с тех пор применён ко многим другим линиям метро и железнодорожным системам по всему миру (CLEARSY).

seL4 — полностью верифицированное микроядро

seL4 — первое в мире полностью формально верифицированное ядро ОС общего назначения (seL4 Foundation).

Метрики:

• 8,700 строк C + 600 строк ассемблера
• 200,000 строк доказательств на Isabelle/HOL
• 20 человеко-лет суммарных затрат (11 — на доказательства seL4, 9 — на фреймворки и инструменты)
• При повторении проекта оценка: ~10 человеко-лет
• Стоимость строки кода: ~*$400* (vs. ~$1,000 для традиционных high-assurance систем)

Что доказано:

• Полная функциональная корректность (от абстрактной спецификации до C-реализации)
• Отсутствие buffer overflow, null pointer dereference, use-after-free
• Гарантии целостности (integrity) и конфиденциальности (confidentiality)

Производительность: 227 циклов на стандартном IPC-бенчмарке (vs. 206 у неверифицированного OKL4 2.1 — разница ~10%).

DARPA HACMS — невзламываемые военные машины

Программа HACMS (High-Assurance Cyber Military Systems) использовала seL4 в автономных транспортных средствах: грузовики, наземные роботы, квадрокоптеры и Boeing Unmanned Little Bird (беспилотный вертолёт) (HACMS Program, PMC).

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

Microsoft — SLAM, P, VCC

• SLAM / Static Driver Verifier (SDV) — формальная верификация Windows kernel-mode драйверов. Использовался для тестирования драйверов, поставляемых с Windows. На лабораторных сессиях участники находили как минимум один баг в своих драйверах (SLAM paper, Microsoft Research)
• P — использован для реализации и верификации USB 3.0 device driver stack в Windows 8.1 (2013). Результат: на 30% более быстрая энумерация устройств, значительно меньше проблем синхронизации (P on GitHub)
• VCC — верификация Microsoft Hyper-V: 100,000 строк конкурентного C-кода + 5,000 строк ассемблера (Verifying Hyper-V with VCC)

Анти-примеры: что случается без формальных методов

Therac-25 (1985–1987) — гибель пациентов

Аппарат лучевой терапии Therac-25 из-за race condition в управляющем ПО дал 6 пациентам смертельные дозы радиации — в сотни раз выше нормы (до 20,000 рад вместо 200). Погибли минимум 3 человека, ещё 3 получили тяжёлые травмы (Wikipedia: Therac-25).

Что пошло не так:

• ПО написано одним программистом на ассемблере PDP-11 без формальной спецификации и независимой проверки
• Аппаратные блокировки (interlocks) заменены программными проверками — без верификации
• Тестирование было минимальным и не покрывало timing-зависимые сценарии
• Race condition проявлялся только при определённой последовательности действий оператора в течение 8 секунд

Урок: именно после Therac-25 safety-critical software engineering стал отдельной дисциплиной, и идея «ПО может заменить аппаратные блокировки» была отвергнута.

Ariane 5, рейс 501 (1996) — $370 миллионов за 40 секунд

Ракета Ariane 5 взорвалась через 40 секунд после старта из-за переполнения при конвертации 64-bit float → 16-bit signed integer в инерциальной навигационной системе. Стоимость потерь: $370 миллионов (ракета + 4 научных спутника). ESA потратила 10 лет и $7 миллиардов на разработку Ariane 5 (Wikipedia: Ariane Flight V88).

Причина: навигационный модуль был переиспользован из Ariane 4 без повторной верификации диапазонов входных значений. Горизонтальная скорость Ariane 5 была значительно выше, чем у Ariane 4, что привело к переполнению.

Мог ли помочь формальный анализ? Да — исследователи показали, что proof-based подход к системной инженерии выявил бы несоответствие диапазонов на этапе проектирования, задолго до первого полёта (Ariane 5 Case Study). Инструменты вроде Astrée обнаружили бы переполнение автоматически.

Разрыв между моделью и реализацией: Weave (Nim)

Проект Weave — высокопроизводительный многопоточный рантайм на Nim (автор — Mamy Ratsimbazafy). Показательный кейс: модель верна, реализация сломана.

Что произошло:

• Backoff-механизм EventNotifier-а (примитив: один потребитель засыпает, несколько производителей будят) специфицирован в TLA+ и проверен model checker-ом на ~10 миллионов состояний — дедлоков не найдено (Weave #18)
• Но при запуске задачи N-Queens (11 ферзей) на 2 потоках — стабильный дедлок (Weave #43)

Три слоя verification gap:

1. TLA+ верифицирует дизайн, а не код — модель корректна, но при переводе в Nim-код (который компилируется в C) допущены ошибки в реализации
2. TLA+ не моделирует hardware memory model — acquire/release семантика атомиков, memory ordering, видимость записей между ядрами невидимы для model checker-а. Как написал автор: «Model checking via TLA+ does not address implementation bugs due to misunderstanding the C11/C++11 memory model for atomics synchronization»
3. Баги в зависимостях — даже корректный код ломается из-за бага в glibc: потерянные wakeup-ы в реализации condition variable (Weave #56, glibc #25847). На macOS проблема не воспроизводилась

Malte Skarupke независимо подтвердил баг glibc через TLA+/PlusCal модель (Using TLA+ to Understand a Glibc Bug, TLA+ модель), позже нашёл второй баг.

Решение: Weave перешёл с glibc condition variables на собственные примитивы на Linux futex, backoff-система переработана и верифицирована заново (релиз v0.2.0 “Overture”).

Урок: формальная верификация модели ≠ корректность реализации. Между TLA+ спецификацией и C/Nim кодом остаётся verification gap — низкоуровневые детали платформы (memory model, OS primitives, багнутые зависимости). Это привело к Nim RFC #222 — предложению инструментов для верификации конкурентного кода прямо в языке.

Ограничения и стоимость формальных методов

Экономика

Формальные методы дороги на входе:

• seL4: 20 человеко-лет на 8,700 строк C — но ~$400/строку (vs. $1,000 для традиционного high-assurance)
• Tokeneer (Praxis/NSA): 10,000 строк high-assurance кода за 260 человеко-дней — ниже стоимости традиционной разработки (Tokeneer)
• Météor: формальная разработка заняла больше времени, но дала ноль багов и 25+ лет без инцидентов — total cost of ownership значительно ниже

Формальные методы экономически оправданы когда:

• Цена бага > стоимости верификации (аэрокосмос, медицина, финансы)
• Система долгоживущая — амортизация стоимости верификации
• Нужна сертификация (DO-178C, Common Criteria)

Барьеры внедрения

По данным опросов индустрии (Cofer et al., 2013, FM Expert Survey, 2020):

1. Образование — 71.5% экспертов считают недостаток подготовки инженеров главным барьером
2. Инструменты — академические, плохо поддерживаемые, не интегрируются в CI/CD
3. Организационная среда — текучка кадров, контракты, давление сроков
4. Масштабируемость — model checking страдает от state explosion на больших системах
5. Скептицизм — восприятие как «дорого, сложно и бесполезно», несмотря на доказанные результаты

Где ФМ не работают (или работают плохо)

• Быстро меняющиеся системы — стоимость поддержания спецификации может превышать пользу
• UI/UX и визуальные системы — формализация затруднена, свойства плохо определены
• Одноразовые скрипты и прототипы — ROI отрицательный
• ML/AI системы — поведение определяется данными, а не спецификацией; верификация в стадии исследований
• Монолитные legacy-системы — слишком дорого специфицировать пост-фактум

Тренд: снижение стоимости

Стоимость формальных методов снижается:

• Lightweight approaches (TLA+ model checking, property-based testing) дают результат за дни, а не годы
• AWS: инженеры продуктивны в TLA+ через 2–3 недели
• LLM начинают генерировать спецификации и proof-аннотации (AutoVerus, VeriCoding)
• Интеграция в языки программирования (Dafny, Verus) убирает разрыв модель/код

Изучение TLA+

Основные ресурсы

Видеокурс Лампорта

TLA+ Video Course — официальный курс от автора TLA+. Покрывает язык, TLC model checker и основы темпоральной логики. Лучшая отправная точка.

Learn TLA+

learntla.com — практический туториал Hillel Wayne. Упор на PlusCal и практические примеры. Хорош как дополнение к видеокурсу.

Specifying Systems

Specifying Systems — книга Лампорта, полный справочник по TLA+. Не для первого чтения — использовать как reference после прохождения курса.

Practical TLA+

Practical TLA+ — книга Hillel Wayne. Более доступное изложение с примерами на PlusCal.

Инструменты визуализации

Spectacle

Spectacle — браузерный model checker для TLA+/Quint. Визуализирует граф состояний прямо в браузере, удобен для небольших моделей и обучения.

TLA+ Graph Explorer

Встроен в VS Code расширение TLA+. Позволяет исследовать state graph после прогона TLC — навигация по состояниям, фильтрация переходов.

TLA+ Animation

TLA+ Animation Module — веб-визуализация trace-ов TLC. Позволяет создавать анимации для наглядной демонстрации поведения модели.

Упражнения по нарастающей сложности

1. Счётчик (Counter)

Цель: освоить базовый синтаксис TLA+/PlusCal, переменные, инварианты.

• Один процесс, инкрементирует переменную от 0 до N
• Инвариант: counter >= 0 /\ counter <= N
• Проверить liveness: <>(counter = N)

2. Mutual Exclusion (Mutex)

Цель: моделирование конкурентных процессов, safety properties.

• Два процесса конкурируют за критическую секцию
• Реализовать алгоритм Петерсона или simple lock
• Инвариант: не более одного процесса в критической секции
• Найти нарушение safety при наивной реализации (без барьеров)

3. Producer-Consumer

Цель: буферизация, fairness, liveness.

• Producer кладёт элементы в bounded buffer, Consumer забирает
• Safety: буфер не переполняется и не уходит в минус
• Liveness: каждый произведённый элемент в итоге потреблён (требует fairness)
• Варьировать количество producer/consumer

4. Two-Phase Commit (2PC)

Цель: распределённые протоколы, отказы, refinement.

• Координатор + N участников, протокол коммита транзакции
• Safety: все участники приходят к одному решению (commit или abort)
• Моделировать отказы участников
• Проверить, что 2PC блокируется при отказе координатора (известное ограничение)

TLA+ vs Lean 4: детальное сравнение

Оба инструмента относятся к формальным методам, но решают принципиально разные задачи. TLA+ — это язык спецификации систем с model checking. Lean 4 — это theorem prover и функциональный язык программирования с зависимыми типами. Сравнение ниже фокусируется на практических различиях для бэкенд-разработчика распределённых и высоконагруженных систем.

Философия и назначение

TLA+: «Что должна делать система?»

TLA+ (Temporal Logic of Actions) создан Лесли Лэмпортом для спецификации поведения конкурентных и распределённых систем. Философия: прежде чем писать код, нужно точно описать что система делает — на уровне абстракции выше кода. TLA+ не пишет и не верифицирует код — он верифицирует дизайн.

Центральная идея: система — это набор допустимых поведений (последовательностей состояний). Спецификация определяет, какие поведения допустимы, а model checker (TLC) исчерпывающе проверяет все достижимые состояния на нарушение заданных свойств (TLA+ in Practice and Theory).

Lean 4: «Можем ли мы это доказать?»

Lean 4 создан Леонардо де Моура (Microsoft Research, сейчас — Lean FRO) как интерактивный theorem prover и одновременно функциональный язык программирования. Философия: код, спецификация и доказательство живут в одном файле и проверяются одним компилятором (lean-lang.org).

Центральная идея: зависимые типы (dependent types) позволяют типам зависеть от значений. Если тип Vector n α — это вектор длины n, то функция head : Vector (n+1) α → α не скомпилируется для пустого вектора — это доказано на уровне типов. Lean устраняет целые классы ошибок (buffer overflow, integer wrap-around) ещё на этапе компиляции.

Спецификация vs Верификация

Ключевое различие: TLA+ работает с конечными моделями системы — model checker перебирает все достижимые состояния и ищет нарушения инвариантов. Если состояний слишком много (state explosion), модель нужно упрощать. Lean 4 доказывает свойства для произвольных входов — нет ограничения конечности, но нужно вручную (или полуавтоматически) построить доказательство.

Язык и синтаксис

TLA+

TLA+ основан на математической нотации: теория множеств, логика первого порядка, темпоральная логика. Выглядит как математика, а не как код:

Init == counter = 0

Next == counter' = counter + 1

Spec == Init /\ [][Next]_counter /\ WF_counter(Next)

TypeOK == counter \in Nat

PlusCal — псевдокодовый слой поверх TLA+, ближе к привычному программированию:

--algorithm counter
variables counter = 0;
begin
  while counter < N do
    counter := counter + 1;
  end while;
end algorithm;

Lean 4

Lean 4 — полноценный функциональный язык с синтаксисом, напоминающим Haskell/ML, плюс тактический язык для доказательств:

def factorial : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

theorem factorial_pos : ∀ n : Nat, 0 < factorial n := by
  intro n
  induction n with
  | zero => simp [factorial]
  | succ n ih => simp [factorial]; omega

Синтаксис Lean ближе к привычному программированию, чем TLA+, но конструкции доказательств (тактики by, simp, omega, induction) — это отдельный навык.

Что именно они верифицируют

TLA+: протоколы и системный дизайн

• Safety: «ничего плохого не происходит» — инварианты, отсутствие дедлоков
• Liveness: «что-то хорошее рано или поздно происходит» — progress, отсутствие livelock
• Распределённые протоколы: Raft, Paxos, 2PC, chain replication
• Конкурентные алгоритмы: lock-free структуры, scheduling, producer-consumer

Конкретный пример: AWS верифицировала алгоритмы DynamoDB (939 строк TLA+), S3 fault-tolerance, EBS volume management. В DynamoDB найден баг с error trace в 35 шагов — невозможно обнаружить вручную (Use of Formal Methods at Amazon Web Services).

Azure Cosmos DB: все 5 уровней консистентности специфицированы и верифицированы в TLA+.

Raft (используется в etcd, CockroachDB, TiKV): формальная спецификация в TLA+ — ~400 строк, является каноническим описанием алгоритма (raft.github.io).

Lean 4: математические доказательства и корректность кода

• Математические теоремы: Mathlib содержит 210,000+ формализованных теорем (на апрель 2025)
• Корректность кода: доказательство, что функция соответствует спецификации
• Безопасность типов: устранение классов ошибок через зависимые типы
• Авторизационные политики: Amazon Cedar — язык авторизации, ядро которого верифицировано в Lean 4

Конкретный пример: Cedar — open-source язык авторизации, лежащий в основе Amazon Verified Permissions и AWS Verified Access. AWS создала формальную модель Cedar в Lean 4 и доказала ключевые свойства корректности и безопасности. Символический компилятор Cedar реализован в Lean и поставляется с доказательствами soundness и completeness (AWS: Lean Into Verified Software Development).

Экосистема и инструменты

TLA+

Ограничения инструментов:

• TLC: не поддерживает liveness в распределённом режиме, не все темпоральные операторы
• TLAPS: не поддерживает рассуждения с вещественными числами и большинство темпоральных операторов
• Apalache: разработка замедлилась после выделения из Informal Systems (конец 2024)

Lean 4

Roadmap Lean FRO (Year 3, август 2025 — июль 2026) (roadmap):

• Стандартная библиотека (Std) 1.0 с async/await, networking, HTTP server
• Новый do-notation интегрированный с workflow верификации
• Кеширование тактик для ускорения итеративной разработки доказательств

Кривая обучения

TLA+: 2–3 недели до продуктивности

По опыту AWS (Newcombe et al.):

• Инженеры осваивают TLA+ за 2–3 недели и начинают находить баги
• PlusCal снижает порог входа — синтаксис ближе к псевдокоду
• На воркшопах участники находят реальные баги к третьему дню
• Главная сложность — не синтаксис, а мышление о состояниях: нужно научиться думать о системе как о множестве допустимых поведений

Ресурсы: видеокурс Лампорта, learntla.com, Practical TLA+.

Lean 4: месяцы, требуется математическая подготовка

По отзывам сообщества (Learning Lean 4):

• «Изучение Lean сложно и временами фрустрирующе» — официальная документация
• Proof assistants — «нельзя ожидать, что станешь продуктивным после одного дня»
• Необходимо понимание зависимых типов, тактик, функционального программирования
• Для математических доказательств: нужна математическая зрелость (индукция, логика, теория типов)
• Для верификации ПО: нужно понимание pre/postconditions, инвариантов, refinement

Ресурсы: Theorem Proving in Lean 4 (TPIL), Functional Programming in Lean (FPIL).

Сравнение кривых обучения

Применение в индустрии

TLA+: стандарт для распределённых систем

• Amazon AWS: S3, DynamoDB, EBS, внутренний distributed lock manager — 7+ команд, 10+ систем (Systems Correctness Practices at AWS, CACM 2024)
• Microsoft Azure: Cosmos DB — все 5 уровней консистентности верифицированы в TLA+
• Alibaba Cloud: формальная верификация распределённых алгоритмов (Alibaba TLA+ Introduction)
• Datadog: формальное моделирование распределённых систем (Datadog Engineering)
• Протоколы: Raft (etcd, CockroachDB, TiKV), Paxos и их вариации имеют каноническую TLA+ спецификацию
• Академия: TLA+ — стандарт для публикации новых распределённых алгоритмов; без TLA+ спецификации статью сложнее принять

Lean 4: математика, AI и верифицированное ПО

• Amazon: Cedar — верифицированный язык авторизации для AWS Verified Permissions и Verified Access (Cedar case study)
• Google DeepMind: AlphaProof — AI для доказательства математических теорем, уровень серебряной медали IMO (VentureBeat)
• Harmonic AI: $100M+ финансирования (2025) — «hallucination-free» AI на базе Lean 4
• Mathlib: крупнейшая в мире формализованная математическая библиотека — 210,000+ теорем
• ACM SIGPLAN Award 2025: Lean награждён за «значительное влияние на математику, верификацию ПО и AI»

Когда что выбирать

Выбирай TLA+ когда:

• Проектируешь распределённый протокол — консенсус, репликация, sharding, failover
• Нужно проверить дизайн до написания кода — найти баги на уровне архитектуры
• Работаешь с конкурентностью — lock-free алгоритмы, message passing, race conditions
• Команда из бэкенд-разработчиков — кривая обучения реалистична (2–3 недели)
• Ограниченное время — TLC даёт результат быстро, без необходимости писать доказательства
• Нужен конкретный контрпример — TLC показывает точный error trace

Выбирай Lean 4 когда:

• Нужно доказать корректность алгоритма для произвольных входов (не ограниченной модели)
• Верифицируешь критический код — авторизация, криптография, парсеры
• Код и спецификация должны жить вместе — нет разрыва между моделью и реализацией
• Работаешь с математическими свойствами — корректность оптимизаций, теоретические гарантии
• Строишь верифицируемый DSL — как Cedar (спецификация + реализация + доказательство)
• Готов инвестировать месяцы в обучение и написание доказательств

Могут ли дополнять друг друга?

Да. TLA+ и Lean 4 работают на разных уровнях абстракции и решают разные задачи — они не конкуренты, а комплементарные инструменты.

Типичный workflow для распределённой системы:

1. TLA+: проверка дизайна — специфицируй протокол, проверь safety/liveness через TLC. Найди и исправь архитектурные баги за дни, до написания кода
2. Lean 4: верификация критических компонентов — для наиболее чувствительных модулей (авторизация, serialization, криптографические примитивы) напиши верифицированную реализацию в Lean с доказательствами корректности
3. Тестирование + мониторинг — для остального кода: property-based testing, fuzzing, runtime-валидация

Пример из реальной практики AWS:

• TLA+ используется для верификации протоколов S3 и DynamoDB (дизайн)
• Lean 4 используется для верификации Cedar (реализация авторизации)
• P используется для state-machine моделирования с генерацией кода

Это три разных инструмента для трёх разных проблем в одной компании.

Резюме: главные различия в одной таблице

Практическая рекомендация для бэкенд-разработчика

Для инженера, работающего с распределёнными и высоконагруженными системами, TLA+ — первый инструмент для изучения. Причины:

1. Прямое попадание в задачу — TLA+ создан именно для спецификации конкурентных и распределённых протоколов
2. Быстрый ROI — продуктивность через 2–3 недели; можно верифицировать текущие рабочие задачи
3. Индустриальный стандарт — AWS, Azure, Alibaba, Datadog используют TLA+ в продакшне
4. Автоматизация — TLC model checker работает без написания доказательств

Lean 4 стоит изучить после TLA+, если:

• Есть потребность в верификации конкретного кода (не дизайна)
• Работаете с авторизацией, криптографией, safety-critical компонентами
• Интересует формальная математика или AI для доказательств
• Готовы к существенным инвестициям времени (месяцы)