Тема: Прикладная часть 4. LLM-дуэль: Верификатор против Имплементора в формальных утверждениях
Уровень сложности: Средний
Расчётное время изучения: 6-8 часов (теория + практика + перенос в capstone)
Предварительные требования: Прохождение части 9 первого тома: проверяемые факты и спецификация направляет, факты допускают к слиянию
Прохождение части 16 первого тома: независимое ревью пакета фактов человеком
Базовое знакомство с JSON Schema и форматом Given/When/Then
Умение запускать Python-скрипты из командной строки
Понимание основ автомасштабирования в Kubernetes (реплики, квоты, лимиты)
Цели обучения: Формулировать инцидентные сценарии в строгом формате Given/When/Then и связывать их с JSON Schema
Строить минимальные контрпримеры: входы, валидные по схеме, но нарушающие утверждение Then
Внедрять протокол LLM-дуэли Верификатор↔Имплементор с фиксацией результатов в validation.md
Преобразовывать найденные контрпримеры в проверяемые next_guard-правила для CI-конвейера
Переводить эксплуатационные границы (квота, лимит, радиус последствий) из устных договорённостей в формальную спецификацию
Обзор: Эта глава учит превращать формально корректные, но опасные запросы в управляемые проверяемые правила через состязательную валидацию. Центральный сценарий — autoscale_200pct: вебхук просит увеличить реплики на 200%, но квота позволяет только 3, а лимит — 15. Вместо ошибки посреди действия система должна либо безопасно ограничить шаг, либо отказать с диагностикой.
Техника LLM-дуэли поручает двум ролям спор по файлам: Верификатор ищет минимальный контрпример, Имплементор чинит правило и реализацию. Спор заканчивается, когда контрпример становится частью спецификации, а повторный прогон выдаёт PASS. Это не ядовитая спецификация (глава 2) и не мутационное тестирование (глава 5) — это проверка устойчивости уже сформулированного правила к конкретным нарушающим входам.
Учебный минимум показывает, как один контрпример превращается в проверяемый вердикт. Полный production-трек добавляет ротацию моделей, ярусы и внешнего Координатора — это материал части 8.
Ключевые концепции: Контрпример: Минимальный вход, который удовлетворяет JSON Schema, но нарушает утверждение Then. Для autoscale_200pct: current_replicas=12, remaining_quota=3, scale_up_percent=200. Минимальность означает, что удаление любого поля уничтожает нарушение. Контрпример публикуется как counterexample.json с полями given_snapshot, when_payload, assertion_id, minimality_trace.
Верификатор: Роль, которая ищет минимальный контрпример к утверждению Then. Побеждает, если строит валидный минимальный контрпример: удовлетворяет входной схеме, но нарушает Then. Не объясняет, а демонстрирует — через воспроизводимый вход.
Имплементор: Роль, которая чинит код и правило после провала дуэли. Побеждает только при двух условиях: обновлены код и правило; повторный прогон дуэли больше не находит тот же класс провала и не ломает существующие инварианты. Обязан выдать четыре артефакта: repair.patch, schema_delta, rationale, affected_assertions.
Минимальность контрпримера: Требование содержать ровно те поля и значения, без которых нарушение исчезает. Плохо: шумовые поля cluster_id, labels, annotations, node_pool, region — при правке неясно, что ломает Then. Хорошо: только current_replicas, remaining_quota, scale_up_percent.
Эксплуатационные границы: Проверяемые ограничения, которые переводят спецификацию из логической плоскости в эксплуатационную: квота (quota), ограничение частоты (rate-limit), радиус последствий (blast-radius), дедупликация, окно повторных действий, максимальный размер изменения. Становятся частью Then: target_replicas <= max_replicas, executed_delta <= remaining_quota / pod_cpu.
Next guard: Новое правило, обязанное проверяться в будущих запусках. Формулируется в Given/When/Then-форме. Пример: «повторный вебхук в течение 2 секунд не увеличивает executed_delta». Превращает единичный инцидент в каталог прецедентов для CI-регрессии.
Validation.md: Журнал дуэлей, хранящий цепочку доказательств: duel_id, assertion_id, проваливающийся случай, версию спецификации до правки, изменение JSON Schema, изменение кода, новый вердикт, ссылку на проход теста дуэли. Не свободный комментарий в тикете, а воспроизводимый регрессионный актив.
Json schema как контракт: Схема ограничивает допустимое пространство входов и связывает поля Given/Then с типами и ограничениями. После контрпримера Имплементор обязан изменить не только код, но и схему — иначе похожие провалы будут проходить.
Координатор: Арбитр, подключаемый, когда Верификатор и Имплементор не сходятся после заданного числа раундов. Проставляет DEFERRED и переводит в manual-review с явным описанием спорного инварианта. Предотвращает бесконечные циклы диагностики.
Реплей соседних случаев: После правки Верификатор обязан переиграть не только исходный контрпример, но и эквивалентные случаи: отсутствующий cluster_id, нулевая квота, повторный вебхук, remaining_quota=1 при current_replicas=max_replicas, конфликт soft_clamp с blast_radius_limit. Защищает от узкой латки.
Практические упражнения: Название: Запуск офлайн-дуэли autoscale_200pct
Проблема: Перейдите в каталог book2/examples/tribunal и запустите скрипт run_duel.py с указанными параметрами. Найдите в выходном файле out/duel.json запись для autoscale_counter_200pct. Определите: какой assertion_id проверялся, какой вердикт получен, какое значение allowed_delta фактически применено, какой diagnostic_code выдан.
Решение: 1. cd book2/examples/tribunal
- python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json
- Откройте out/duel.json, найдите объект с counterexample_id: "autoscale_counter_200pct"
- Проверьте поля: assertion_id должно быть "allowed_delta_within_quota", verdict — "PASS"
- В actual найдите: allowed_delta: 3 (ограничено квотой), diagnostic_code: "QUOTA_EXCEEDED_AFTER_CLAMP"
- Убедитесь, что вход валиден по схеме (scale_up_percent=200 в диапазоне 1-1000), но Then выполняется через ограничение, а не через полное удовлетворение запроса
Сложность: beginner
Название: Проверка минимальности контрпримера
Проблема: Дан контрпример: {current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200, cluster_id: "agentclinic-prod", namespace: "appointments", labels: {team: "platform"}, node_pool: "standard", region: "us-east-1"}. Сократите до минимального. Объясните, почему удалённые поля не влияют на нарушение, и сформулируйте критерий минимальности для вашего случая.
Решение: 1. Удалите cluster_id — нарушение остаётся (проверка квоты не зависит от идентификатора кластера)
- Удалите namespace, labels, node_pool, region — нарушение остаётся
- Удалите pod_cpu — нарушение исчезает: без pod_cpu невозможно вычислить floor(remaining_quota / pod_cpu), формула allowed_delta ломается
- Минимальный контрпример: {current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200}
- Критерий минимальности: удаление любого из четырёх полей делает нарушение невоспроизводимым
Сложность: intermediate
Название: Формулировка next_guard для high_memory_usage
Проблема: Перенесите принцип из autoscale_200pct в capstone-проект. Сценарий: при high_memory_usage правило restart_pod разрешает dry-run, если readiness >= 23/25. Но stateful-под с backup_verified=false нельзя перезапускать даже при readiness=24/25. Постройте минимальный контрпример и сформулируйте next_guard в Given/When/Then-форме.
Решение: 1. Минимальный контрпример: readiness=24/25, stateful=true, backup_verified=false
- Проверка минимальности: удаление stateful=true — нарушение исчезает (readiness >= 23/25 разрешит dry-run); удаление backup_verified=false — нарушение исчезает (stateful=true + backup_verified=true допустимо); удаление readiness=24/25 — нарушение исчезает (при readiness < 23/25 dry-run и так заблокирован)
- Формулировка next_guard: "Given stateful=true и backup_verified=false When readiness >= 23/25 Then dry-run заблокирован с диагностикой STATEFUL_BACKUP_REQUIRED"
- Запись в validation.md:
duel_id: duel-high-memory-001 assertion_id: HM-READINESS-01 counterexample: "readiness=24/25, stateful=true, backup_verified=false" verdict: PASS next_guard: "Given stateful=true и backup_verified=false When readiness >= 23/25 Then dry-run заблокирован с диагностикой STATEFUL_BACKUP_REQUIRED"
Сложность: intermediate
Название: Анализ ошибки процедуры: только код, без схемы
Проблема: Верификатор нашёл контрпример autoscale_200pct. Имплементор изменил только код, добавив формулу allowed_delta в Python-функцию, но не обновил JSON Schema — поля max_actions_per_window и clamp_policy остались вне required. Через неделю пришёл новый вебхук с отсутствующим clamp_policy, система упала в ошибку. Где ошибка в процедуре дуэли? Какой артефакт Имплементор не выдал?
Решение: 1. Ошибка: Имплементор нарушил условие победы — не обновил правило (спецификацию и схему), а изменил только код
- Отсутствующий артефакт: schema_delta — изменение JSON Schema, которое закрепило бы новые поля политики ответа
- Почему это важно: схема — это контракт, проверяемый до выполнения. Без схемы новый вход с отсутствующим clamp_policy проходит валидацию и ломается в рантайме
- Правильная процедура: Имплементор обязан выдать repair.patch (код), schema_delta (схема), rationale (обоснование), affected_assertions (список затронутых утверждений)
- Повторный прогон должен включать соседний случай: отсутствующий clamp_policy, конфликт soft_clamp с blast_radius_limit
Сложность: advanced
Название: Построение CI-конвейера с дуэлью
Проблема: Сформируйте последовательность команд для CI, которая: (1) валидирует схему, (2) запускает дуэль с лимитом 8 раундов, (3) требует наличия next_guard в validation.md. Объясните, почему третий шаг — lint_validation.py — необходим, и что произойдёт, если Верификатор найдёт новый контрпример в середине спринта.
Решение: 1. Шаг 1: python3 scripts/spec_ci/lint_spec.py spec/incident-autoscale.md — проверяет синтаксис и связанность полей с JSON Schema
- Шаг 2: python3 scripts/tribunal/run_duel.py --scenario autoscale --case autoscale_counter_200pct.json --max-rounds 8 --out .artifacts/duels/autoscale.json — запускает дуэль с ограничением раундов
- Шаг 3: python3 scripts/spec_ci/lint_validation.py validation.md --require next_guard — проверяет, что каждый провал породил проверяемое next_guard-правило
- Зачем lint_validation.py: без него контрпример останется в out/duel.json — локальном артефакте, — а не превратится в регрессионный актив. CI не заблокирует повторение того же класса ошибки
- Если Верификатор найдёт новый контрпример в спринте: конвейер должен потребовать schema_delta, обновления правила, повторного зелёного прохода. Красный статус недостаточен — нужен воспроизводимый след в validation.md
Сложность: advanced
Кейсы: Название: AgentClinic-production: autoscale_200pct и квотный провал
Сценарий: В кластере AgentClinic-production работает сервис appointments-api. Загрузка CPU 98%, реплик 12, квота позволяет добавить ещё 3, лимит реплик — 15. Прилетает вебхук от Grafana: «увеличьте количество реплик на 200%». Формально просьба корректна — все поля заполнены, диапазоны валидны. Выполнение требует 12 дополнительных реплик (200% от 12), но квота — 3, а лимит — 15.
Задача: Два сценария реакции: (1) правило проверяет только формальную корректность входа — автоскейлер уходит в ошибку посередине действия, частично создав реплики и нарушив консистентность; (2) правило не включает эксплуатационные границы в Then — квота, лимит, радиус последствий считаются «очевидными» и не проверяются формально. Команда обнаруживает, что один и тот же класс ошибок повторяется при разных входах: нулевая квота, max_replicas=current_replicas, duplicate webhook.
Решение: Внедрение LLM-дуэли Верификатор↔Имплементор. Верификатор строит минимальный контрпример: current_replicas=12, remaining_quota=3, scale_up_percent=200. Имплементор отвечает формулой allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) и политикой hard_block | soft_clamp. Ключевой шаг: формула закрепляется в JSON Schema через новые поля max_actions_per_window и clamp_policy, которые становятся required. Повторный прогон дуэли включает соседние случаи: отсутствующий cluster_id, нулевая квота, повторный вебхук внутри дедупликационного окна, remaining_quota=1 при current_replicas=max_replicas. Каждый провал и победа фиксируются в validation.md с duel_id, assertion_id, next_guard.
Результат: Система переходит из режима «ломаться на проде» в режим «отказывать с диагностикой до изменения состояния». Контрпример autoscale_counter_200pct получает verdict PASS с diagnostic_code QUOTA_EXCEEDED_AFTER_CLAMP и allowed_delta=3. Новый вебхук с теми же параметрами обрабатывается за 50 мс с чёткой диагностикой, без частичных изменений. CI-конвейер блокирует регрессию: если новый код возвращает старое правило без clamp_policy, lint_validation.py выдаёт ошибку. Команда накапливает 12 записей в validation.md за квартал, покрывающих квотные, частотные и дедупликационные провалы.
Извлечённые уроки: Минимальный контрпример ценнее объяснения: он воспроизводим и проверяем автоматически
Эксплуатационные границы должны быть в Then, а не в устных договорённостях — иначе каждый новый инженер их переоткрывает
Имплементор обязан менять схему вместе с кодом: schema_delta — не опция, а условие победы
Соседние случаи в реплее защищают от узкой латки, которая закрывает один пример и оставляет эквивалентный провал
validation.md превращает единичный инцидент в каталог прецедентов, который CI использует для регрессионной защиты
Связанные концепции: Контрпример
Верификатор
Имплементор
Минимальность контрпримера
Эксплуатационные границы
next_guard
validation.md
Реплей соседних случаев
Название: Перенос принципа в capstone: high_memory_usage и stateful-блокер
Сценарий: Студент проходит учебный трек и должен перенести принцип autoscale_200pct в собственный capstone-проект. Его сценарий: при высокой загрузке памяти правило restart_pod разрешает перезапуск, если readiness >= 23/25. На проде обнаруживается, что stateful-под с непроверенным бэкапом (backup_verified=false) перезапускается при readiness=24/25, теряя состояние.
Задача: Студент копирует контрпример autoscale_200pct вместо формулировки принципа. В capstone/validation.md появляется запись про current_replicas и remaining_quota — поля, нерелевантные для restart_pod. Ревьюер отклоняет: контрпример не минимален, next_guard не применим к домену. Нужно построить свой минимальный контрпример и сформулировать next_guard, сохраняя структуру, но меняя содержание.
Решение: Анализ структуры из autoscale_200pct: минимальный контрпример содержит только поля, без которых нарушение исчезает; next_guard формулирует новое правило в Given/When/Then; эксплуатационная граница переводит ограничение из устного в проверяемое. Для high_memory_usage: минимальный контрпример — readiness=24/25, stateful=true, backup_verified=false. Проверка минимальности: удаление stateful=true или backup_verified=false убирает нарушение. next_guard: «Given stateful=true и backup_verified=false When readiness >= 23/25 Then dry-run заблокирован с диагностикой STATEFUL_BACKUP_REQUIRED». Эксплуатационная граница: restart_pod не расширяется до namespace-уровня.
Результат: Студент осваивает перенос принципа, а не копирование. Запись в capstone/validation.md принята ревьюером. При последующем расширении правила на namespace-level restart студент автоматически получает конфликт с next_guard и вынужден либо ослабить guard явно (с обоснованием), либо сохранить ограничение. Это предотвращает неявное расширение радиуса последствий.
Извлечённые уроки: Перенос из учебного кейса в capstone — это формулировка принципа, не копирование данных
Минимальность проверяется по домену: для autoscale это квота, для restart_pod — stateful + backup
next_guard создаёт будущее трение: любое расширение правила вынуждено взаимодействовать с записанным ограничением
Структура validation.md универсальна: duel_id, assertion_id, counterexample, verdict, next_guard применима к разным доменам
Связанные концепции: next_guard
Минимальность контрпримера
Эксплуатационные границы
validation.md
Советы по изучению: Начинайте с офлайн-прогона: cd book2/examples/tribunal && python3 scripts/run_duel.py. Увидеть PASS в stderr — быстрый выигрыш, который мотивирует разбирать детали
Перед чтением теории запустите скрипт и сломайте его: удалите поле clamp_policy из входа, посмотрите, где именно падает — так поймёте, почему схема важнее кода
Используйте технику «шумовое поле»: добавьте в контрпример cluster_id, labels, annotations — убедитесь, что дуэль всё ещё находит нарушение. Потом убирайте по одному, пока не найдёте минимум. Это ручная проверка того, что Верификатор делает автоматически
Ведите параллельный validation.md вручную, до автоматизации: запишите duel_id, assertion_id, контрпример, next_guard бумагой или в редакторе. Сравните с выводом lint_validation.py — поймёте, какие поля машина проверяет строго, а какие оставляет на трактовку
Для визуального стиля: нарисуйте блок-схему из пяти шагов (Given/When/Then → Верификатор → Имплементор → Реплей → validation.md) и повесьте рядом с рабочим местом. При каждом новом инциденте проходите по ней — выработаете мышечную память
Для аудиального стиля: диктуйте Given/When/Then вслух перед записью. Если фраза не укладывается в три строки — спецификация ещё не готова к дуэли
Для кинестетического стиля: моделируйте дуэль ролями с коллегой. Один — Верификатор, ищет контрпример, другой — Имплементор, чинит за 5 минут. Таймбоксинг показывает, где процедура застревает
Сравнивайте с пройденным: вернитесь к части 9 (проверяемые факты) и части 16 (ревью человеком). Контрпример в дуэли — это автоматизированное ревью, которое происходит до слияния, а не после
Откладывайте production-сложности: ротация моделей, ярусы, Координатор — материал части 8. Сейчас фокус на одном раунде по одному правилу. Не распыляйтесь
Проверяйте себя контрольными вопросами в конце главы: зачем минимальность, почему объяснение не заменяет доказательство, что меняет Имплементор кроме кода, где ошибка если только код без схемы
Дополнительные ресурсы: Examples/tribunal/readme.md: Локальный runnable-аналог дуэли с инструкциями по запуску и ожидаемым выводом
Examples/tribunal/specs/autoscale spec.yaml: Учебная спецификация autoscale с Given/When/Then и JSON Schema
Examples/tribunal/cases/autoscale counter 200pct.json: Минимальный контрпример для прогона
Examples/tribunal/scripts/run duel.py: Скрипт офлайн-дуэли для учебного прохождения
Book/part-09-feature-validation.md: Проверяемые факты и «спецификация направляет, факты допускают к слиянию»
Book/part-16-team-code-review.md: Независимое ревью пакета фактов человеком
Github spec kit: https://github.com/github/spec-kit — практика specification-first в SDD
Wikipedia: formal specification: https://en.wikipedia.org/wiki/Formal_specification — Given/When/Then как формальная спецификация
Judgment.example.md: Пример оформления вердикта с согласованием counterexample_id и assertion_id
Резюме: LLM-дуэль Верификатор↔Имплементор превращает формальную спецификацию в управляемый механизм проверки инцидентных решений. Ключевой результат — не абстрактная проверка текста, а рабочий протокол из четырёх шагов: инцидентный сценарий связан с JSON Schema, спорные условия проверены минимальными контрпримерами, эксплуатационные лимиты стали частью спецификации, каждый провал зафиксирован как воспроизводимое улучшение в validation.md.
Главная ценность — в эксплуатационных границах. Квота, ограничение частоты, радиус последствий переводятся из устных договорённостей в проверяемые Then-утверждения. Автоматическая ремедиация не подменяет безопасность формально правильным, но опасным действием.
Учебный минимум требует три артефакта: Given/When/Then-сценарий, связанный со схемой; минимальный counterexample.json или запись в validation.md; сформулированный next_guard в Given/When/Then-форме. Полный трек добавляет repair.patch, schema_delta, матрицу соседних контрпримеров и локальный smoke-pass.
Перенос в capstone — формулировка принципа, не копирование. Из autoscale_200pct берётся структура минимальности и next_guard, а содержание строится под домен high_memory_usage или собственный проект.