Инвойс был мёртв. А потом списал твои деньги.

Состояния, которые нельзя удалить

Инвойс аннулировали. Деньги при этом уже списали.

Все тесты зелёные. Тип правильный. Ни одного ограничения в базе, которое бы это запрещало. Его просто никто не додумался поставить — никто и не знал, что такое состояние вообще возможно. Оно жило во времени: аннулируешь инвойс — а следом с опозданием прилетает платёжный вебхук и подтверждает списание, которое уже было в пути. Обработчик проверял payment_succeeded? и не додумался спросить voided?. Запись прошла, в реестре ноль к оплате, а реальное списание висело несведённым.

Это Часть 2. Часть 1 удалила баги, которые можно удалить: размеченное объединение, ограничение в базе, недопустимые состояния, которые ты делаешь невыразимыми. А это тот, что остался: ни одной неправильной строки кода, переписывать нечего. Всё, что можно сделать, — спросить, достижимо ли плохое состояние, и если да, отгородить его забором.

Так я его и нашёл. Вместо того чтобы гадать, какие комбинации опасны, я задал чекеру один вопрос: а voided + paid вообще достижимо? Он выдал путь, draft → finalized → voided → voided + paid, который никто не рисовал на доске и не проигрывал ни один тест. В этом весь приём. Чекер не просто держит забор — он подсказывает, какой забор строить, чтобы ты точно знал, куда поставить CHECK.

Типы удаляют плохие состояния, ограничения удаляют плохие комбинации, но запретить можно только те состояния, о которых ты уже знаешь. И ни то ни другое не трогает порядок, в котором приходят события. А кое-что вообще не влезает ни в тип, ни в CHECK: пространство состояний слишком велико, или бизнес не даёт его ужать, или весь баг — это последовательность переходов, а не какая-то одна строка.

Для таких режешь дальше. Есть короткая лестница инструментов верификации. Каждая ступень чуть дороже предыдущей и покупает гарантию посильнее. Конечный автомат, генератор пар, чекер моделей — с виду не связаны, но каждый задаёт один и тот же вопрос со всё большей строгостью: может ли случиться плохое состояние и насколько мы в этом уверены? Все четыре гонять не нужно — лезешь вверх, пока что-нибудь не поймает твой баг, и там останавливаешься. Сначала самые дешёвые:

Шаг 1 — Конечные автоматы

Кто-то выставляет isPublished в true. Забывает сбросить isArchived. Тип это позволяет, никто не проверяет — и над живым объявлением вылезает баннер «в архиве». Булево выставили; инвариант — нет.

Конечный автомат делает этот переход недостижимым ещё до того, как он случится: он заранее объявляет, какие переходы вообще существуют, и отвергает всё, чего в списке нет. Черновик может стать опубликованным. Опубликованный — уйти в архив. Архивный вернуться в черновики не может. Никогда. Ничему в кодовой базе не нужно «помнить» правило: автомат отвергает всё, чего нет в таблице, а строки «опубликован и в архиве разом» в таблице попросту нет.

Автомат в этом вопросе уверен куда больше, чем роадмап.

# Ruby с AASM
class Order < ApplicationRecord
  include AASM
  aasm do
    state :draft, initial: true
    state :published, :archived
 
    event(:publish) { transitions from: :draft, to: :published }
    event(:archive) { transitions from: [:draft, :published], to: :archived }
    # Обрати внимание: обратного перехода из :archived нет. Архив — терминальное состояние.
  end
end
 
order.publish!   # OK
order.archive!   # OK из draft или published
archived_order.publish!  # AASM::InvalidTransition — автомат сказал нет

И вот теперь автомат — это разом и документация, и обеспечение. Достижимые состояния конечны, лежат в одном месте, а всё, чего нет в таблице, просто отвергается. Правила ты записываешь один раз — дальше их гоняет за тебя автомат. Граф и есть тип.

Шаг 2 — Сэмплируй пространство

Когда пространство слишком велико, чтобы перечислить его целиком, а ужать сильнее уже нельзя, — его сэмплируют, и есть два способа: один грубый, другой точный.

Грубый — это property-based тестирование, и я сам годами на него забивал: написать хорошие свойства всегда казалось возни больше, чем просто подобрать пару входов руками. И зря.

Фишка простая. Вместо «вход X → выход Y» ты объявляешь свойство, которое должно держаться для любого входа, а фреймворк забрасывает его сотнями случайных кейсов, пытаясь сломать: fast-check (TypeScript), Hypothesis (Python), PropCheck (Ruby). Stateful-варианты ещё и бродят по случайным последовательностям переходов. Он играючи обходит те три кейса, что ты выбрал бы сам. Но у случайности есть слепое пятно: та самая пара, что тебя топит, — ровно то место, куда ни один бросок так и не попадает.

Другую половину этого слепого пятна я тоже отгружал: баг, который жил только в состоянии, которого наши тестовые данные ни разу не создавали. Контент приходил в двух видах с разными правилами по времени, а сид-скрипты генерировали только один — так что вторая ветка ни разу не прогонялась в CI, и исключение, возможное только в ней, уехало зелёным. Пространство состояний, которое обходили наши тесты, было строгим подмножеством того, в котором работает прод.

Точный способ закрывает это слепое пятно по построению — и число почти неприличное.

Двадцать фича-флагов — это 1 048 576 возможных конфигураций. Проверить каждую их пару можно за десять тестов.

1 048 576 → 10. Каждая пара из двадцати флагов — в десяти конфигах.

Не тысяча. Десять. И это не фокус: десятилетия данных о сбоях говорят, что сбои кучкуются во взаимодействиях немногих факторов. Разбор реальных багов от NIST показал, что проверка каждой пары ловит 70–97 % багов, и по всем изученным ими наборам данных о сбоях ни одному не требовалось больше шести взаимодействующих факторов разом.

Так что покрываешь ты не миллион конфигов, а пары — и пары умещаются в десять строк. Покрывающий массив — это небольшой набор конфигураций, гарантирующий, что каждая пара значений встретится хотя бы раз. А если нужно поймать конкретную тройную комбинацию — подними силу до t = 3, и она ляжет в строки по построению.

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

Покрывающие массивы

32 конфига → 6

dark-mode и pdf-export по отдельности работают. Включи оба — и PDF рендерится белым по белому, невидимка. Баг прячется в одной паре флагов, среди 32 конфигов. Поймаешь?

🎲 Бросить кости

dark-modepdf-exportnew-navbeta-bannercompact

1·····

21111·🐛

311··1🐛

4··111

51·1··

6·1·1·

1 = вкл · · = выкл · 🐛 = баг

ПОЙМАЛ ✓6 конфигов покрывающего массива включают каждую пару, так что плохая пара всегда внутри.

Почти никто так не делает: открытый репозиторий GitLab несёт около пятисот фича-флагов, тестирует их по одному, без всякого попарного покрытия между ними, — а ведь с флагами они аккуратнее большинства из нас. Ты в хорошей компании. Баг тоже.

A B C
0 0 0
0 1 1
1 0 1
1 1 0

dark-mode-for-real:   on, off
ai-everything:        on, off
temporary-fix-2019:   on, off
layout:               single-page, multi-step
 
IF [ai-everything] = "on" THEN [dark-mode-for-real] = "off";

from allpairspy import AllPairs
import pytest
 
flags = {
    "dark_mode_for_real": [True, False],
    "ai_everything":      [True, False],
    "temporary_fix_2019": [True, False],
}
 
@pytest.mark.parametrize("cfg", AllPairs(list(flags.values())))
def test_checkout(cfg):
    dark_mode_for_real, ai_everything, temporary_fix_2019 = cfg
    assert checkout_works(dark_mode_for_real, ai_everything, temporary_fix_2019)

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

Значит, у сэмплирования есть потолок. А хотелось-то мне перестать бросать кости и доказать, что свойство держится на каждом достижимом состоянии. Оказывается, можно.

Шаг 3 — Проверка моделей (формальная верификация)

Один баг проходит сквозь все предыдущие подрезки. Он проходит проверку типов, переживает пару сотен бросков property-теста и читается на ревью чисто — потому что его нет ни в одной строке кода. Он в порядке, в котором приходят два события, в переплетении, которое никто не рисовал на доске. Он ждёт — а потом будит тебя в 3 ночи, где искать его дороже всего. Это и есть тот самый баг, который переживает все тесты.

Model checking создан именно под этот баг. Property-тесты сэмплируют — чекер моделей обходит всё пространство целиком. Даёшь ему точное описание своей системы, каждое состояние и каждый переход, и он посещает каждое достижимое состояние этого описания, а потом кладёт тебе на стол ту самую последовательность, что ломает твоё правило. Две оговорки. Обходит он только то описание, что ты ему дал, а не твой реальный код, — а значит, хорош ровно настолько, насколько честно это описание совпадает с тем, что ты выкатил. И обходит он только тот мир, который ты ограничил (два инвойса, один вебхук), полагаясь на то, что баг, которому нужны четыре объекта, всё равно вылезет и в маленькой версии. Обычно так и есть; это гипотеза малого масштаба, и на ней тихо держится всё остальное.

AWS гоняет TLA+ на S3 и DynamoDB с 2011-го. seL4 (ядро, доказанное корректным вплоть до ассемблера) летает в дронах. Продолжение от AWS 2025 года прямолинейно: в одиночку ни один инструмент не вытянул, понадобился целый набор. Урок: бери самый дешёвый инструмент, который исчерпывает твоё пространство состояний.

Самый маленький полезный пример умещается на салфетке. Возьми Todo с четырьмя состояниями — active, done, archived, deleted — и одним правилом: раз удалено — удалено навсегда. TLC обходит каждое достижимое состояние и подтверждает, что правило держится, — все до единого, а не горстку кейсов.

Выигрыш виден, когда коллега добавляет безобидный с виду переход «отменить удаление». Компилируется на любом языке; property-тест его может и проворонить. А TLC ловит мгновенно — и не просто говорит «упало». Он отдаёт точную кратчайшую последовательность, которая ломает правило: active → deleted → active. Model checker возвращает не красный крестик, а фильм о том, как система ломается. Поиграй ниже: аннулируй счёт — а платёж, уже бывший в пути, приходит позже и вытаскивает его из могилы со штампом PAID. Прибивай зомби, пока они вылезают, — тех, за кем не уследил, упустишь, — потом жми «Рентген» и смотри, как чекер моделей доказывает порядок, который оплачивает мёртвый счёт, каждый раз:

Проверка моделей

Прибей призрака

Аннулируй счёт — он мёртв, похоронен. Но платёж, уже бывший в пути, приходит позже, и счёт выбирается из могилы со штампом PAID. Прибивай зомби, пока не сбежали. (За всеми пятью могилами разом не уследить…)

🔨 Начать🔎 Рентген (проверка модели)

Посмотреть полную спецификацию — открыть редактор

Чтобы понять это, не нужно читать ни строчки TLA+.

На Todo это выглядит перебором — для обычного CRUD размеченное объединение и так ловит почти всё, что нашёл бы чекер. Именно поэтому его и отмахивают как «академическое», и именно в этом ошибка. Баги, которые переживают все дешёвые подрезки, в CRUD не живут. Они живут в порядке и конкурентности: ретраи платежей, выборы лидера, два вебхука, дерущиеся за одну и ту же строку, — те переплетения, которые не описывает ни одна отдельная строка кода.

Писать спеку стало дёшево — доверять ей нет

Цена формальных методов никогда не была в чекере. TLC и Z3 бесплатны и на этом масштабе отрабатывают за секунды. Цена была в спеке: написать её должен был кто-то с редким знанием. Вот это и изменилось. Теперь спеку набрасывает LLM, а чекер моделей вроде TLC — или SMT-солвер вроде Z3 — заменяет многолетнее доказательство для всего, что меньше космического аппарата.

Барьер рухнул сразу с двух сторон.

С одной стороны — генерация. LLM теперь пишут вполне сносный TLA+, и есть готовые скиллы Claude Code на всю петлю: напиши спеку, запусти TLC, разбери нарушение. Честной её держит одна дисциплина — истина в последней инстанции чекер, а не модель. LLM с радостью выдаст правдоподобную спеку, которая втихую окажется учебниковым Paxos, а не твоей системой. Неправильная спека, уходящая в красное, стоит тебе минут; настоящий риск — та, что уходит в зелёное, потому что чекер ручается только за ту спеку, которую ему скормили. Так что генерация не убирает человека. Она сдвигает твою работу с написания спеки на её чтение: минуты вместо лет.

С другой стороны — извлечение. Если твой автомат уже живёт в коде, спеку не нужно ни писать, ни даже генерировать. Твой блок aasm, твой XState-автомат, твой редьюсер уже и есть спека; пара сотен строк экстрактора поднимают их в формат входа чекера. Эту рутину я и автоматизировал, а саму идею можно попробовать прямо сейчас в браузерном плейграунде.

Так или иначе, узкое место сдвинулось — не исчезло, а сменило форму. LLM набрасывает спеку, превращает твой код в валидный TLA+ и даже подкидывает кандидатов в инварианты, чтобы чекер их принял или опроверг. Чего она не сделает — не скажет тебе, какое свойство вообще стоит утверждать; а это и есть проектная работа, собственно вся работа.

Бенчмарк 2026 года (Can LLMs Model Real-World Systems in TLA+?), где топовые модели пишут TLA+ по коду реальных систем, проводит границу чётко: синтаксис они берут почти всегда, но инвариант для проверки им по-прежнему подаёт человек — и даже тогда спека честно совпадает с работающей системой меньше чем в половине случаев. Машина это записывает; а что значит «правильно» и что там получилось — решаешь и вычитываешь по-прежнему ты. Вот эта часть и превратилась из редкой экспертизы в привычку, за которой тянешься, — вечер, а не PhD. (PhD всегда был явным перебором, чтобы проверить: можно ли всё ещё заплатить по аннулированному счёту.)

Ветки, что пережили ревью

Баги, которые реально стоят денег, — кросс-полевые: инвойс помечен voided, а его payment_status всё ещё succeeded — деньги списаны по отменённому счёту, мимо реестра. Ни одна строка не написана неправильно; просто у двух полей статуса нет правила, запрещающего эту комбинацию. Сложи два конечных автомата и спроси, достижимо ли запрещённое совместное состояние, — и получишь кратчайший путь, который туда ведёт:

✗ VoidedIsNeverPaid — voided and payment=succeeded must not co-occur.
    counterexample (reachable from the initial state):
      status = draft,     payment_status = pending
      status = finalized, payment_status = pending
      status = voided,    payment_status = pending
      status = voided,    payment_status = succeeded   ← the bug, as a reachable path

Этот путь — и есть весь смысл. Ты получаешь точную последовательность шагов, которая приводит в нелегальное состояние, так что баг приходит с уже приложенными шагами воспроизведения.

Этот пример я не выдумал. Я навёл небольшой чекер на две широко развёрнутые open-source денежные системы — биллинговый движок и коммерс-платформу — и он вытащил ровно эти противоречия. Достижимый путь — это кандидат, а не баг: чекер работает от объявленного конечного автомата, так что гард, которого он не видит (коллбэк, условная запись), может сделать «достижимое» состояние недостижимым в работающей системе. И это не пустые слова: со мной так и случилось — это та самая стена, в которую упирается вся техника. Так что слово «баг» кандидат заслуживает только тогда, когда ты воспроизвёл его на настоящей системе, — а оба этих как раз воспроизвелись, каждый на развёрнутом слое (обработчик платёжного вебхука, роут админки), каждый закрылся однострочным гардом.

Одно честное замечание про масштаб. На одной строке voided + succeeded настолько грубо противоречивы, что и чекер не нужен, чтобы понять их незаконность, — same-row CHECK (NOT (status = 'voided' AND payment_status = 'succeeded')) запрещает это напрямую. Чекер начинает окупаться на шаг дальше: когда два факта лежат в разных строках (списание приходит в отдельную строку payments через миг после аннулирования), где ни одно однострочное ограничение не видит обе половины разом, и весь баг — это порядок, в котором они пришли. Вот до этого случая CHECK сам не дотянется; это и есть место, где дешёвая подрезка начинает буксовать.

И этот класс багов — не моё открытие: исследование ISSTA 2011 нашло кросс-полевые ошибки модели данных ровно этой формы в двух реальных Rails-приложениях за пятнадцать лет до того, как я навёл на это решатель. Это латентные баги — вскрытые ограниченной проверкой, а не живыми авариями. И это тоже реальные денежные пути.

Сам чекер — небольшой open-source инструмент: извлеки конечный автомат, который у тебя уже есть, и спроси, достижимо ли плохое состояние (prune-states). Но инструмент тут дело десятое — смысл в том, чтобы эти подрезки легли в твою кодовую базу раньше, чем ты напишешь следующий булев флаг.

Где дешёвая подрезка упирается в стену

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

Опасные баги обычно живут по другую сторону, в dataflow: поле, записанное на пути, который проскочил гард; коллбэк, втихую переключивший состояние за спиной модели; неверно пересчитанный баланс. prune-states сам упёрся в эту стену. Один инвариант дал ложное срабатывание, потому что коллбэк менял состояние, невидимое для модели уровня объявлений. Баг тут — не достижимое состояние, а запись, дошедшая до легального состояния неправильным путём. Отследить это статически, анализом мест записи и потребителей, всё ещё целый проект, а не однострочник.

Поэтому ты и не воюешь с ним там, а меняешь слой, со времени компиляции на время выполнения, где путь перестаёт что-либо значить. CHECK в базе срабатывает на самой записи, так что неправильный путь, приведший к нелегальной строке, ловится, как бы он туда ни попал: ограничение проверяет запись, а не путь, который её породил. А вот что всё равно проскальзывает — это запись «неправильная, но легальная»: баланс, пересчитанный в значение, которое ограничение спокойно пропускает, — и конкурентность, которая его порождает. Это уже не формы, которые ты запрещаешь, — это гонки, которые ты делаешь безопасными: ключ идемпотентности, transactional outbox, правильный уровень изоляции.

Это не значит, что на dataflow ты сдаёшься. Просто меняешь тактику: перестаёшь доказывать, что путь безопасен, и начинаешь следить за самой записью. Работа-то одна и та же: назвать инвариант, а потом отдать его чему-то понадёжнее внимательного программиста. А когда подрезки сделаны, есть ход дешевле, чем делать их заново в следующем квартале: не дать пространству состояний тихо отрасти обратно.

Забюджетируй пространство состояний

Самый дешёвый баг состояния — тот, который так и не добавили. Останавливаешь его, делая цену видимой в тот самый момент, когда за состоянием тянутся.

Мы строили CRM, когда кто-то вполне резонно предложил дать пользователям настраивать всё через визуальный интерфейс: триггеры, действия, даже схемы таблиц — всю модель данных, а не только значения. Никто не сказал нет — потому что никто в комнате не думал о пространствах состояний; думали о свободе выбора для пользователя, а это вещь и правда хорошая. Но «пользователь настраивает модель данных» означало, что каждая комбинация триггера, цепочки действий и схемы становилась состоянием продукта, которое мы обязаны обрабатывать, — не большое пространство, а неограниченное, своя топология на каждого клиента. Мы месяцами пилили инфраструктуру ради гибкости, которая никому не была нужна, а no-code-довод, которым это оправдывали, испарился в тот момент, когда PM смог описать схему LLM и получить её за тридцать секунд. Сложность пережила аргумент, который её построил.

Вот форма всего этого: не ошибочное решение, а разумный аргумент, высказанный до того, как кто-нибудь достал число. Out of the Tar Pit называет цену точно: каждый добавленный бит состояния удваивает число возможных состояний; сложность перемножается, а не складывается. Но разовый довод «это добавляет неограниченно много состояний» — потраченный капитал против структуры стимулов, которая награждает того, кто зашипил фичу, а не того, кто считал её состояния. Эту битву не выиграть, споря громче. Её выигрывают, делая цену фоновой.

Дай пространству состояний бюджет, как ты бюджетируешь размер бандла: CI-бот, который пишет в PR коммент «это изменение добавляет два булевых поля в CheckoutProps: 32 состояния → 128». Шипи его как информацию, а не гейт: гейт отключают в первый же раз, когда он блокирует фичу из роадмапа, а число в PR проживёт достаточно долго, чтобы поменять смысл слова «нормально». Это дешевле того, что приходит потом: багов, которые ты не можешь воспроизвести, и команды, которую ты в итоге наберёшь, чтобы отвечать на вопрос «а как вообще должна выглядеть настройка у этого клиента?».

Начни подрезать

Статические подрезки ты уже сделал — Часть 1 — или начни сперва с них. Это слой верификации.

На этой неделе. Возьми фича-флаги, которые твой тест-сьют гоняет по одному. Сгенерируй покрывающий массив. Шесть строк вместо миллиона; та пара, что тебя ломает, ляжет туда по построению. А если эти флаги можно вместо этого удалить в размеченное объединение — сделай сначала это: багу, который нельзя записать, никакой тест не нужен.

В этом месяце. Возьми один из своих конечных автоматов — AASM, XState, редьюсер — и выпиши кросс-полевой инвариант, который он подразумевает, но нигде не обеспечивает. Проверь, достижимо ли это состояние. Руками или небольшим чекером. Дай своему пространству состояний бюджет: CI-коммент, который до любого мёржа показывает «это изменение добавляет два булевых поля: 32 состояния → 128».

Каждая подрезка мала. Каждая удаляет класс багов навсегда. Сложи несколько — и твои выходные перестанут прерывать.

Часть 1 мы открыли таймлайном, ветвящимся из-под контроля, — твоим, а теперь ещё и модели. Две статьи спустя: плохие состояния нельзя записать, а те, что уцелели, — недостижимы. Ветку, которую тип не может собрать, нельзя зашипить; состояние, до которого чекер не может добраться, не уронит прод. И тогда ничто, прошедшее все тесты, уже не кладёт прод.

Подрежь таймлайн. По одной подрезке за раз.

Источники