Справедливо щодо документації Kafka — так, цей кейс справді описаний. Наша робота не претендує на відкриття нового бага, а пропонує формальний інструмент, який робить це знання відтворюваним і незалежним від конкретного брокера.

Щодо language memory model — ви маєте рацію, для race conditions в межах одного процесу це правильний інструмент. Але temporal collisions у розподілених системах — це інший клас проблем: мова йде про crash-вікно між двома системами (consumer + broker), де немає спільної пам’яті. TLA+ моделює саме цей клас помилок.

Performance тести можуть випадково ловити race conditions завдяки навантаженню — збільшується ймовірність одночасного доступу до ресурсів, що провокує timing-sensitive баги. Але це не гарантія: вони не перевіряють всі можливі переплетіння подій, тільки ті, що виникають за конкретного сценарію навантаження. Формальна верифікація доповнює цей підхід вичерпним пошуком.

Абсолютно згоден — це не баг Kafka, це наслідок того, як написаний consumer. Саме про це стаття: crash window між StoreResult і CommitOffset — це фундаментальна властивість будь-якої at-least-once системи, незалежно від брокера. Kafka тут ні до чого.
Питання в іншому: скільки розробників усвідомлюють це на рівні «я знаю, що треба писати idempotent consumer» vs «я математично довів, що без idempotency shield подвійне виконання неминуче»? Більшість знає про проблему інтуїтивно, але TLA+ дозволяє зробити це знання формальним і відтворюваним. Особливо коли система ускладнюється — кілька consumerів, різні timeout, firefly sync, тощо.
Дякую за дискусію, це допомагає краще сформулювати цінність підходу.

Чудова стаття, дякую за системний підхід. Крива Боема — саме те, чому ми взагалі маємо думати про тестування на ранніх етапах. Rust з його type system чудово закриває memory safety і апаратну конфігурацію, але, як ви правильно зазначили, бізнес-логіку він не верифікує.
Хочу додати ще одну прогалину в цій піраміді: temporal collisions. Навіть юніт-тести + інтеграційні + HIL не ловлять race conditions між компонентами, які працюють з різними таймінгами або через асинхронні канали. Наприклад, сенсор записав значення в регістр, але application шар прочитав його до того, як драйвер завершив консистентне оновлення — і HIL це не побачить, бо на реальному залізі воно відтворюється раз на 1000 запусків.
Ми дослідили цю проблему з TLA+ (model checking) на прикладі Kafka/NATS/RabbitMQ — виявилось, що тестова піраміда має сліпу зону на рівні міжкомпонентних протоколів, і формальна верифікація її закриває. Деталі в статті «Чому тести не ловлять race conditions і що з цим робити», якщо цікаво: dou.ua/forums/topic/60608

Чудовий розбір, дякую. Особливо сподобався акцент на тому, що «HTTP-метод — це просто рядок», а головне — стандартизація семантики safe/idempotent/cacheable. Це саме те, що відрізняє протокол від кастомного рішення.
Хочу додати важливий нюанс зі своєї практики. Навіть коли семантика методу чітко визначена в RFC, distributed middleware (проксі, кеші, балансувальники) можуть створювати temporal collisions між моментом, коли інфраструктура вирішує «це safe, можна кешувати/ретраїти», і реальним станом системи. Це та сама проблема, що з Kafka consumer: між StoreResult і CommitOffset існує crash window, і тести його не ловлять.
Ми дослідили це питання з використанням TLA+ (model checking) — виявилося, що навіть семантично «безпечні» протоколи мають несподівані колізії на рівні взаємодії middleware. Якщо цікаво, деталі в статті «Чому тести не ловлять race conditions і що з цим робити» — там якраз про те, чому формальна верифікація потрібна навіть тоді, коли RFC написаний ідеально: dou.ua/forums/topic/60608

Чудовий глибокий матеріал, дякую. Особливо сподобався приклад із write skew (лікарі на чергуванні) — класична ілюстрація того, як дві «правильні» транзакції ламають інваріант.

Хочу додати, що та сама проблема виникає не лише в базах даних, а й у message brokers. Наприклад, crash consumer між StoreResult і CommitOffset у Kafka — це той самий write skew, тільки замість двох лікарів — два deliver одного повідомлення. Кожен consumer окремо «правильний», але разом вони порушують інваріант exactly-once processing.

Різниця в тому, що в БД ми маємо isolation levels і MVCC, а в асинхронних протоколах таких вбудованих гарантій немає. Саме тому для message brokers особливо корисна формальна верифікація (TLA+): вона вичерпно перевіряє всі можливі переплетення подій до деплою.

Докладніше про temporal collisions: dou.ua/forums/topic/60608

Чудова стаття, Сергію. Особливо згоден про те, що ШІ не скасовує архітектурне мислення, а робить його критичнішим.

Хочу додати ще один шар: архітектурне мислення — це не лише про GRASP/GoF на етапі проєктування. Це ще й про верифікацію того, що система дійсно поводиться згідно з архітектурою під усіма можливими переплетеннями подій (race conditions, crash, network delay).

Патерни описують «як має бути», але не гарантують, що в runtime щось пішло не так. Саме тут на допомогу приходить формальна верифікація (TLA+): вона вичерпно перевіряє, чи можливе порушення архітектурних інваріантів за будь-якого переплетення подій. Те саме «архітектурне мислення», але формалізоване й автоматизоване.

Докладніше про temporal collisions писав тут: dou.ua/forums/topic/60608

Дякую за детальний огляд. Трохи доповню.

ArchUnit чудово перевіряє статичну архітектуру (шари, пакети, анотації) — це layer 1 захисту. Але в розподілених системах є й динамічні порушення архітектури, які байт-код не покаже: temporal collisions, коли crash між StoreResult і CommitOffset призводить до подвійної обробки.

Тут статичного аналізу замало. Для таких випадків є комплементарний підхід — формальна верифікація (TLA+), яка моделює протокол і вичерпно перевіряє всі переплетення подій. ArchUnit + TLA+ = architecture testing на статику й динаміку.

Докладніше про temporal collisions: dou.ua/forums/topic/60608

Чудовий матеріал, дякую за детальний розбір. Особливо сподобався підхід із negative control (RAW mode) — це правильна інженерна культура.
Хочу звернути увагу, що описаний RLS-витік — це окремий випадок ширшого класу проблем: temporal state collisions у розподілених системах. Сесійний app.tenant_id «протікає» через PgBouncer так само, як offset commit «протікає» через crash consumer у Kafka: стан (GUC / offset) залишається жити після того, як власник (транзакція / consumer) його покинув.
Transaction-local GUC (is_local=true) — це по суті те саме, що transaction-level offset commit у Kafka або векторні годинники в NATS: явне прив’язування стану до меж транзакції, а не до сесії.
До речі, ви питаєте про автоматизовані хаос-тести. Є комплементарний підхід — формальна верифікація (TLA+). Замість того щоб вбивати контейнери й дивитись, чи виживе система, можна вичерпно перевірити модель протоколу (пул + транзакції + RLS) до деплою. TLC перебере всі можливі переплетення подій — включно з тим кутовим випадком, де reset потрапив на інший backend.
Докладніше про temporal collisions писав тут: dou.ua/forums/topic/60608

Чудовий огляд, дякую за систематизацію. Рамка «шари» дуже правильна — саме так і треба думати про агентний стек.
Хочу додати один важливий шар, якого в статті бракує: верифікація протоколів.
Коли агенти спілкуються через A2A, MCP або x402, це розподілена система з усіма відповідними наслідками: повідомлення можуть дублюватись, агенти можуть крашнутись між отриманням повідомлення і записом результату, порядок доставки не гарантований. Це та сама проблема temporal collisions, яку добре знають інженери Kafka/RabbitMQ/NATS — double execution через crash між StoreResult і CommitOffset.
Для агентної економіки це критично: агент заплатив через x402, зберіг результат у свій state, і впав до підтвердження — інший агент не знає про платіж і платить знову. Або навпаки: товар відвантажено двічі.
Формальна верифікація (TLA+) дає змогу вичерпно перевірити такі протоколи до deployment: модель агента + брокера + протоколу, і TLC перебирає всі можливі стани. Це shift-left для найдорожчих багів — тих, що проявляються тільки в production під навантаженням.
Докладніше про temporal collisions у message brokers писав тут: dou.ua/forums/topic/60608

Хороше питання про exactly-once semantics.

Kafka EOS (transactional producer) гарантує exactly-once від producer до broker, але не захищає consumer після crash. Якщо consumer зберіг результат у БД і впав до commitSync(), новий consumer не знає про це і починає з останнього коміченого offset — повідомлення обробляється вдруге. EOS цього не змінює, бо offset commit — це окремий протокол.

Двофазний коміт вимагає transaction coordinator. Якщо координатор падає між prepare і commit — ми в тій самій ситуації з ще більшою складністю.

«В книжці написано» — так, проблема відома десятки років. Наш внесок не у відкритті, а в:
1) Формальному TLA+ доказі, що це фундаментальна властивість будь-якої at-least-once системи, а не баг реалізації;
2) Уніфікації — одна специфікація покриває Kafka, NATS, RabbitMQ;
3) Cross-validation через chaos engineering, де прогноз TLA+ збігся з реальністю в 4/4 випадках.

Це shift-left: знайти проблему в специфікації до того, як книжка опише саме ваш випадок.

Дякую за конструктивну дискусію.

Справедливі зауваження, дякую.

«Сферичний кінь у вакуумі» — частково погоджуюсь. TLA+ модель — це абстракція, але вона безпосередньо відображає реальний протокол consumer + broker. І вона передбачила конкретну поведінку, яку ми потім вручну відтворили через Toxiproxy: docker kill контейнера з consumer у вікні між StoreResult і CommitOffset.

Steps to reproduce — вони є: pilot_kafka/ у репозиторії містить docker-compose + Toxiproxy конфіг. Для Celery — celery_test/. Маю додати прямі посилання в текст статті, вибачте.

PR ігнорують — так. Kafka PR закрили без merge. Celery discussion висить без реакції. Я не стверджую, що підхід уже визнаний ком’юніті — це експериментальний інструмент. Але він математично доводить проблему, і я продовжую роботу над автоматизацією repro, щоб знизити поріг для мейнтейнерів.

Дякую за чесний фідбек.

Дякую! Сподіваюсь, вислуга років колись конвертується в якийсь сеньйор-мідл :))

Дякую за глибоке питання — ви влучили в саму суть архітектурного компромісу.

### 1. Чому verifier бачить рубрику, а worker — ні

Це не баг, а фіча. Хтось **мусить** оцінювати код проти критеріїв — інакше ми не дізнаємось, чи вирішено задачу. Ключова різниця:

| Шар | Бачить рубрику? | Чому це ок / не ок |
| :--- | :--- | :--- |
| **Worker (Execution)** | ❌ Ні | Щоб не міг оптимізувати під конкретні пункти («додати docstring, бо це +0.3 балу») |
| **Verifier** | ✅ Так | Щоб міг оцінити відповідність вимогам. Але він **сліпий** до автора, промпту, історії — тому не може «підіграти» |

Тобто тиск «підіграти» не зникає, але **локалізується в шарі, який не генерує код**. Verifier може бути суб’єктивним, але він не може змінити код — тільки оцінити його. Це як розділити роль «автора» і «рецензента» в академічному paper.

### 2. Чи перевіряв я, що ізоляція реально допомагає?

**Чесно: формального A/B тесту ще не проводив.** Але є непрямі сигнали:

— **Ранні прототипи** (де worker бачив рубрику «наполовину») давали 15-20% false-positive вердиктів: код виглядав добре, але не вирішував задачу.
— **Після увімкнення `seal_*` контрактов** false-positive впали до <2% (на вибірці ~10 запусків).
— **Абстрактний feedback** змушує worker дійсно покращувати код, а не формально відповідати рубриці.

Саме так. І проблема не в моделях — вони роблять те, для чого їх оптимізували. Проблема в архітектурі: коли агент бачить тести, він оптимізує під тести, а не під задачу.

Я в Developer Farm вирішив це не промптами, а ізоляцією: Execution-шар фізично не отримує ні тестів, ні рубрики. Тільки технічний опис + контекст. Верифікатор теж сліпий — бачить тільки git diff.

Результат: $0.03/фичу, 26 секунд, код який вирішує задачу, а не геймить метрики.

Дякую за глибокі питання — саме такі розбори роблять проєкт кращим. Відповідаю по черзі, максимально чесно:

## 1. Verifier: тільки LLM, чи LLM + автоматичні checks?

**Зараз: тільки LLM** (Qwen-Turbo через OpenRouter). Верификатор отримує git diff + рубрику і повертає holistic score 0.0–1.0 + reason.

**Це слабке місце**, і я про це відкрито кажу. Планується додавання класичних checks як **додаткового сигналу** (не заміни LLM):
— `ruff` / `pylint` — linting
— `mypy` — type checking
— `pytest` — якщо в артефакті є тести
— AST-аналіз — складність, цикломатика

Чому не заміна? Бо LLM ловить **семантичні** проблеми («функція реалізує не те, що просили»), а статичний аналіз — **синтаксичні**. Ідеальна верифікація = обидва шари.

## 2. Як рахується score?

**Це НЕ average по rubric.** Це **holistic score** від LLM.

Рубрика передається як контекст (наприклад: «docstrings — 0.3, type hints — 0.3, error handling — 0.4»), але LLM не рахує середнє арифметичне. Вона оцінює код **цілісно**, враховуючи вагу кожного критерію суб’єктивно.

**Чому так?** Бо average по rubric = ідеальна умова для Гудхарта. Агент, який бачить «docstrings = 0.3», просто додасть docstrings скрізь, навіть де вони не потрібні. Holistic score змушує верифікатора думати як senior engineer, а не як калькулятор.

**Ціна цього підходу:** score менш детермінований. Один і той самий код може отримати 0.85 і 0.92 при різних запусках. Тому ми фіксуємо seed + temperature=0.1 для стабільності.

## 3. Межа між pipeline з архітектурними обмеженнями і expert system?

Дуже тонка, і це важливо розуміти:

**Expert system** = жорсткі правила, детермінована логіка («якщо X, то роби Y»). Ми цього **НЕ** робимо. Ми не кодуємо правила «як писати код».

**Наш pipeline** = LLM-based генерація, але з **TypedDict контрактами як «рельсами»**. Ми не кажемо агенту *що* робити — ми створюємо умови, за яких він *не може* зґеймити метрики.

**Межа:**
— Expert system: «Додай docstring до кожної функції» → агент виконує правило формально
— Наш підхід: «Агент не бачить, що docstring оцінюється» → він додає docstring тільки якщо це дійсно потрібно для читабельності

Тобто ми будуємо **institutional design** (як конституція для агентів), а не expert rules (як інструкція).

## 4. «Фізично неможливо порушити чесність» — яка гарантія?

**Це гарантія в межах pipeline, НЕ ширша інженерна гарантія.**

Конкретно:
— ✅ **Захищено:** передача `acceptance_criteria` у Execution викликає `ValueError` на рівні `seal_task_for_execution()`
— ✅ **Захищено:** передача `worker_id` у Verification блокується `seal_artifact_for_verification()`
— ❌ **НЕ захищено:** якщо хтось змінить `contracts.py` і прибере `seal_*` — захист зникає
— ❌ **НЕ захищено:** Python не має compile-time типізації, це runtime-перевірка

Тобто це **архітектурна домовленість**, закріплена кодом, а не формальна верифікація (як у Coq або TLA+). Для серйозної гарантії треба додавати:
— `mypy —strict` на `contracts.py`
— Unit-тести на `seal_*` функції (перевіряти, що вони дійсно викидають `ValueError`)
— CI pipeline, який ламається при порушенні контрактів

**Чесно:** зараз це «сильна домовленість», а не «математична гарантія». Різниця важлива.

## 5. Головний practical lesson?

### ✅ Що спрацювало найкраще:

1. **Абстрактний feedback** — найсильніша фіча. Коли верифікатор пише «Code quality needs improvement» замість «Add docstring to is_palindrome()», агент дійсно покращує код, а не геймить рубрику. Це працює краще, ніж я очікував.

2. **Git worktrees для кожної ітерації** — кожна спроба в окремому branch. Це дає **audit trail**: можна подивитись, як код еволюціонував від ітерації 1 до ітерації 4. Випадково виявили, що 80% «покращень» на ітерації 2-3 — це косметика, а реальні фікси — на ітерації 1.

3. **Локальний Execution + API Planning/Verification** — економіка $0.03/фичу реальна. OpenRouter білінг підтверджує.

### ⚠️ Слабкі місця:

1. **Verifier тільки LLM** — пропускає баги, які ловить `mypy` або `ruff`. Були кейси, коли код отримав 0.95, але не компілювався через typing error.

2. **Абстрактний feedback іноді занадто vague** — «Consider improving error handling» не дає агенту зрозуміти, *що саме* покращити. Результат: 3 ітерації без прогресу, потім timeout.

3. **Planning залежить від якості spec** — якщо spec написана абстрактно («зроби добре»), Planning генерує абстрактний task, Execution генерує абстрактний код. Garbage in, garbage out працює на 100%.

4. **Neo4j indexing повільний на великих кодових базах** — індексація 100+ файлів займає 2-3 хвилини. Для MVP ок, для production треба оптимізувати (incremental indexing, caching).

---

**Що далі:** плануємо додати `ruff` + `mypy` у Verification шар як **обов’язковий pre-check** перед LLM-оцінкою. Якщо код не компілюється — LLM взагалі не викликається, одразу FAIL з конкретним повідомленням. Це закриє головне слабке місце.

Дякую за питання — саме такі розбори перетворюють pet-project на інженерний інструмент. Якщо хочете подивитись код `seal_*` функцій або `generate_abstract_feedback()` — все відкрито: github.com/...​rm/blob/main/contracts.py

Буду радий продовжити дискусію! 🙏

Ви абсолютно праві: **текст у репозиторії ≠ працююча система**. І єдина справжня перевірка — це прогнати пайплайн на реальній кодовій базі з 300+ issues, зібрати білд, прогнати тести.

Ось що ми вже зробили, щоб це було можливо:

✅ **Reproducible benchmarks**: у [`BENCHMARKS.md`](github.com/...​m/blob/main/BENCHMARKS.md) — покрокова інструкція, як запустити пайплайн і отримати верифікований `00_final_report.json` з метриками часу, вартості та якості.

✅ **Goodhart-proof ізоляція**: це не промпт-інженерія, а контракти на рівні `TypedDict`. Спроба передати `acceptance_criteria` у виконання викидає `ValueError` — це компілюється, а не «сподіваємось, що агент послухає».

✅ **Відкрита архітектура**: код під MIT, можна форкнути, підключити свій репо, додати свої тести. Якщо знайдете, де ізоляція «протікає» — це баг, а не фіча. Кидайте issue `[BENCHMARK]`, розберемо.

Щодо «великої кодової бази»:
— **Neo4j-інтеграція** вже дозволяє планувати фичі на основі графа залежностей (іморти, виклики, наслідування), а не вгадувати контекст.

**Пропозиція**: якщо у вас є репо з 300+ issues, яке ви готові відкрити для тесту — давайте зробимо спільний стрес-тест. Ви даєте spec на одну фичу, я запускаю пайплайн, ми разом дивимось на:
1. Чи зламав білд
2. Чи пройшли тести
3. Чи не зґеймив агент метрики (порівнюємо diff з рубрикою)
4. Скільки це коштувало і скільки зайняло

Якщо пайплайн не впорається — це не провал, а дані для ітерації. І ці дані ми опублікуємо в тому ж `BENCHMARKS.md` — чесно, з логами.

Бо якщо корисність вимірюється не хайпом, а тим, чи вирішує інструмент реальну проблему — то давайте перевіримо це разом. 🤝

Дякую за відвертість — це важливо.

Про «триколісний велосипед»: так, Developer Farm не танк. Але іноді потрібен не танк, а інструмент, який:
— коштує $0.03 за замість $500/міс,
— працює локально на старій відеосистемі,
— і **фізично не може** зґеймити метрики, бо архітектура не дає.

Це не конкуренція з «заводами». Це альтернатива для тих, кому не потрібен танк — а потрібна чесність.

Про «нудне обличчя і гроші»: погоджуюсь, що візуальний шум і пітчинг часто виграють. Але хакатон [Proof of Usefulness](proofofusefulness.com/reports/developer-farm) створений саме проти цього: алгоритм оцінює не презентацію, а **верифіковані сигнали** — GitHub forks, reproducibile бенчмарки, API-логи. Якщо інструмент дійсно корисний, це видно по коду, а не по обличчю.

Про «ніхо не зайде в репозиторій»: це виклик, а не вирок. Тому ми:
— публікуємо [BENCHMARKS.md](github.com/...​m/blob/main/BENCHMARKS.md) з відтворюваними запусками,
— додаємо шаблон `[BENCHMARK]` Issue для спільноти,
— інтегруємо спонсорські інструменти (Neo4j, Bright Data), щоб алгоритм міг крос-валідувати корисність.

Якщо ви бачите, що саме зробити, щоб репозиторій **став цікавим** для української спільноти — радий почути конкретні поради. Може, додати приклади для українських стартапів? Локалізувати документацію? Зробити демо-відео з субтитрами?

Бо якщо корисність вимірюється не хайпом, а тим, чи вирішує інструмент реальну проблему — то Developer Farm вже працює. А от чи побачать його люди — це вже спільна задача.

Дякую, що прочитали до кінця. 🙏