Згоден — малий приклад це мінімум, а повна дисципліна — доводити властивості самого визначення. І тут ми вашу схему фактично застосували: у Bridge.lean наше представлення діаграм доведено еквівалентним незалежному представленню Mathlib (hookLen_eq_YD) — «друга сторона» тут зовнішня бібліотека, а не LLM, що частково знімає і ваш пункт про конфлікт інтересів.

Щодо «навіщо руками» — «руками» означало «не на слово ШІ», брутфорс так само годиться. Але перебір перевіряє скінченну кількість випадків, а ваші властивості isdiag — всі одразу, тобто це вже доведення, і саме цим займається Lean.

І чесно: soundness-баги в ядрах асистентів знаходили (Coq, Lean 3 у 2022) — «доведено» завжди «відносно коректності ядра й аксіом», що лише підсилює тезу статті.

Влучна метафора, але вона працює в обидва боки — і в цьому суть.

«Доведи аксіому сам» — саме так, і це рівно та точка, де ми зупинилися. Але важливо, які це аксіоми: у проєкті лишилися не «LLM не змогла пояснити», а конкретні відкриті задачі з теорії коефіцієнтів Кронекера (зокрема для повної no-go теореми Бюржіссера—Ікенмаєра—Панової). Це відомі нерозв’язані проблеми — їх не довів ні людина, ні модель. Довести їх «самому» — це повноцінна дослідницька програма, а не один крок.

А щодо «проекції 3D на площину» — чесне занепокоєння, і я його не відкидаю. Так, плоска відповідь LLM може бути тінню чогось глибшого. Але рівно тому формальна перевірка й існує: інтуїцією неможливо відрізнити «проекцію повного рішення» від «переконливого шуму», який звучить упевнено. Гіпотеза проекції перевіряється єдиним способом — спробою довести аксіому до кінця. «Можливо, там щось є» — легітимна гіпотеза, але вона не зараховується як «доведено». Саме тому в статті й написано: компілятор перевіряє узгодженість формулювання, а не його відповідність реальності.

Дякую за змістовний коментар! Кілька уточнень з практики.

1. Щодо поєднання ролей «розробника» і «тестувальника» — у випадку Lean це працює інакше, ніж у звичайному QA. «Тестувальник» тут — ядро Lean: механічна машина, якій байдужий результат і в якої немає мотивації щось «підробити». Конфлікт інтересів, про який ви кажете, реальний для людського тестування, але не для формального чекера. Проблема ж ховається не в кроці перевірки, а у формулюванні — і саме тому головний контрприклад у статті вбиває не помилка доведення, а порожнє визначення `P_equals_NP := True`. Компілятор перевіряє узгодженість того, що йому подали, — а не відповідність реальності.
2. Ідея «два агенти: один формулює, другий доводить» слушна саме для етапу формулювання. Але важливо тямити обмеження: два LLM мають скорельовані упередження, тож це не гарантія. Найсильніший «другий агент» — формальне ядро плюс незалежний перерахунок на малому прикладі руками (саме так зловили помилку C(2k,k)→k у статті).
3. Про «навчалися на простих задачах — шукають прості рішення» — згоден, і це рівно причина, чому фінальний урок статті такий: перевіряй на конкретному малому прикладі, руками, перш ніж довіряти узагальненню.

Дякую, тут суть заперечення зовсім інша, і вона справедлива в широкому сенсі — essential complexity Брукса нікуди не поділась, і я не пропоную формалізувати 60%+ вимог усього проєкту перед розробкою.

Але зверніть увагу на масштаб того, що конкретно формалізується. Це не бізнес-логіка, не еволюційні вимоги продукту — це одна вузька, стабільна властивість самого протоколу доставки повідомлень (at-least-once + crash-window), яка не залежить від того, наскільки визначені бізнес-вимоги вашого конкретного проєкту. Семантика доставки Kafka/RabbitMQ/NATS не змінюється щоспринту разом із вашим product backlog — вона фіксована дизайном брокера. Тобто це не top-down специфікація всієї системи, а point verification одного ізольованого, добре зрозумілого шматка інфраструктури.

І тут є показовий контрприклад до тези «формальні методи працюють лише на військових/атомних/космічних проєктах з чіткими вимогами» — це AWS, компанія, максимально далека від waterfall. Самі інженери AWS описують свій підхід так: вони пишуть звичайний prose-документ дизайну, а потім інкрементально уточнюють окремі його частини в PlusCal чи TLA+ — часто це дає важливі інсайти, навіть не доходячи до повної специфікації чи model checking. Вони самі визнають: команда прагне уникати зайвої складності, але essential complexity задачі залишається високою — тобто той самий Брукс, та сама проблема, яку ви описали. Але це не завадило TLA+ дати їм відчутну практичну користь саме тому, що застосовувався він локально й вибірково — на конкретних критичних алгоритмах (S3, DynamoDB, EBS), а не на всій системі одразу.

Щодо «ідеї Дейкстри провалились» — тут я б розрізнив дві різні речі. Повний ручний доказ коректності (Дейкстра, Хоар) справді не масштабувався в індустрії — це правда. Але TLC/model checking — це якраз відповідь на цей провал, а не його повторення: замість повного доказу — вичерпний автоматичний перебір скінченної абстракції вузького шматка системи. Це вже інший клас інструменту з іншою історією індустріального застосування, і саме тому я не намагаюсь «врятувати» ідею Дейкстри в повному обсязі — я використовую вужчий, вже перевірений на практиці її нащадок, саме в тому масштабі, де він історично працює.

«Exactly-once» у Kafka — це реальна гарантія, але вона діє всередині транзакційного домену самої Kafka: атомарний запис у топік + producer-транзакція + offset commit, або класичний read-process-write цикл (Kafka Streams). Це підтверджує і сама документація: транзакції підтримуються лише всередині одного Kafka-кластера, і якщо в межах транзакції є процесори із зовнішньо спостережуваними побічними ефектами, потрібні додаткові компоненти — тут може допомогти transactional outbox pattern.

Сценарій у статті — саме цей «зовнішній побічний ефект»: консюмер пише результат у Postgres, окрему систему поза Kafka. Щойно консюмер взаємодіє з будь-якою зовнішньою системою, він виходить за межі транзакційного домену Kafka — і якщо збій стається між записом у БД і offset commit, Kafka при відновленні повторно доставляє те саме повідомлення, а застосунок повторно його обробляє; Kafka, не маючи жодного уявлення про вашу БД, не може цьому запобігти. Вона зробила свою роботу. Це відомо як dual-write problem: запис у Kafka (offset commit) і запис у зовнішню систему — це два окремі записи, які не можна виконати атомарно; якщо один з них падає незалежно від іншого, ви ризикуєте отримати дублікати або втрачені оновлення.

Тобто «exactly-once» з документації Kafka технічно правильна цитата, але вона не покриває саме той кейс, що змодельований у статті — не тому, що я неправильно зрозумів Kafka, а тому що ця конкретна межа (Kafka-транзакція ↔ зовнішня БД) — задокументована архітектурна межа самого exactly-once, а не моя інтерпретація.

Щодо Essential Complexity (Брукс):
Брукс має рацію: складність ПЗ неминуча. Але TLA+ не намагається подолати цю складність — він працює з конкретною властивістю: «чи можлива ситуація, коли дві нитки виконають одне завдання двічі?»
Це не формалізація всієї системи. Це формалізація протоколу з 3-5 кроків:
1. Consumer отримує повідомлення з брокера
2. Consumer зберігає результат у БД
3. Consumer комітить offset/back-ack брокеру
Crash window — між кроками 2 і 3. Якщо consumer падає тут, брокер перенаправляє повідомлення іншому consumer, який не знає про крок 2. Результат: двічі виконане завдання.
TLA+ перевіряє: чи існує хоча б одне переплетіння дій, що веде до execCount=2 для одного повідомлення? Відповідь: так, для будь-якої at-least-once системи з crash-вікном. Це математичний факт, а не імовірнісна оцінка.

Щодо Дейкстра:
Дейкстринський weakest precondition calculus перевіряє коректність коду — чи реалізація відповідає специфікації. TLA+ перевіряє архітектуру — чи специфікація взагалі допускає небезпечний стан.
Це різні рівні:
— Дейкстра: «чи цей цикл правильно сортує?» → код
— TLA+: «чи можлива ситуація, коли два consumer оброблять одне повідомлення?» → протокол
«Вічний двигун» Дейкстра — це про неможливість формалізувати все ПЗ. Ми не формалізуємо все — ми формалізуємо одну критичну властивість конкретного протоколу. Це не амбітна спроба замінити тестування — це доповнення до нього на рівні «чи безпечна моя ідея до написання коду?»

Практичний результат:
Ми знайшли конкретний баг у Celery (ACK timeout при ETA-задачах у Redis), який жив у продакшені роками. TLA+ модель показала, що double-execution досяжний при timeout < visibility_timeout. Chaos-тест підтвердив: docker kill контейнера з consumer у crash-вікні → повідомлення оброблене двічі.
Це не теорія — це конкретний баг з конкретними кроками відтворення. І він стосується не одного проекту, а будь-якої at-least-once системи з ack-протоколом: Kafka, RabbitMQ, NATS, Celery, BullMQ.

Щодо Kafka — ви праві в тому ж сенсі, що і Vitaliy та Serhii вище: at-least-once і механізм redelivery — це свідомий дизайн, не збій Kafka. Але зверніть увагу: сам механізм, який ви описали («Kafka чекає ACK, якщо його нема — перенаправляє повідомлення») — це і є те, що спричиняє дубль виконання, коли side-effect консюмера (запис у Postgres) не ідемпотентний. Kafka робить рівно те, що мала робити за протоколом — і саме тому виникає execCount=2. Тобто це не «помилка розуміння Kafka» з мого боку, а якраз опис того, як Kafka влаштована — я моделюю не збій брокера, а взаємодію двох коректно працюючих компонентів (брокер за протоколом + консюмер, що ще не встиг закомітити offset).

Щодо другого пункту — «TLA+ показує можливість інциденту до нього, це безглузде твердження» — тут, здається, плутанина між двома різними речами: прогнозуванням і доведенням досяжності стану.
TLC не прогнозує, коли саме станеться інцидент, і не оцінює його ймовірність. Він вичерпно перебирає всі можливі переплетіння дій, дозволені специфікацією протоколу, і доводить: чи існує серед них хоча б одна послідовність, що веде в заборонений стан (execCount=2). Це логічний доказ досяжності, зроблений аналітично — без запуску коду, без продакшена, без єдиного реального consumer’а. «До того» означає буквально «до написання коду» — TLC знаходить контрприклад ще на етапі специфікації.

Те, що інцидент «неминучий» (ваш пункт 3, погоджуюсь) — не робить це доведення марним. Навпаки: якщо властивість фундаментальна і невід’ємна від at-least-once семантики (а не implementation bug, який можна «запобігти» патчем), то формальний доказ цього — саме те, що дозволяє свідомо спроектувати мітигацію (idempotent consumer) до деплою, а не з’ясувати це постфактум через дублікати в БД. Детекція постфактум і доведення досяжності до деплою — це різні речі не тому, що один «запобігає», а інший «детектує» в сенсі ймовірності, а тому що один дає вам конкретний контрприклад (яку саме дію послідовності треба заблокувати guard’ом) до того, як хтось написав перший рядок consumer-коду.

Alex, дякую за детальну аргументацію. Ви праві в одному: всередині одного процесу event state machine = простий граф, де correctness доводиться per-node. Але мова статті про міжпроцесний crash window.

Конкретний кейс:
1. Consumer отримує івент з Kafka
2. Consumer пише в PostgreSQL (змінює стан)
3. Consumer падає (docker kill, OOM, мережа)
4. Kafka не отримала ACK → перенаправляє івент іншому consumer’у
5. Два consumer’и записали в одну таблицю → double execution

Ваша відповідь: " система має мати recovery by design". Але recovery ≠ запобігання. Recovery = виявлення + компенсація після того, як double execution вже стався. А TLA+ доводить, що crash window існує до написання коду.

Логи показують дуплікати після інциденту. TLA+ показує можливість інциденту до нього. Це різні рівні: один = детекція, другий = запобігання.

питання в тому, як переконатися, що архітектура дійсно правильна, коли система складна: кілька consumer’ів, різні timeout’и, кілька брокерів.

Приклад: RabbitMQ docs описують at-least-once delivery, але не гарантують відсутності double execution при crash до ACK. Це не баг — це документована поведінка. Але інженер може не знати про це, поки не трапиться інцидент.

TLA+ не замінює досвід — він дає математичний доказ того, що конкретна конфігурація безпечна. Як unit test для архітектури: можна і без нього, але з ним — впевненіше.

Погоджуюсь — для досвідченого інженера це очевидно. А як ви перевіряєте свою event-driven архітектуру на race conditions перед деплоєм?

Згоден, статичний аналіз ловить помилки проєктування. TLA+ доповнює це формальною верифікацією протоколів — перевіряє не код, а архітектуру.

Alex, дякую за детальний коментар. Ваш підхід цікавий — event sourcing, де івент = зміна стану. Але crash window не зникає, він переміщується на рівень системи.

Конкретне питання: якщо consumer обробив івент (змінив стан) і крашнувся ДО того, як система «дізналася» про це (через heartbeat, reconciliation, saga compensation) — що відбувається?

Якщо система не виявила крах → інший нод може підхопити той самий івент → подвійна обробка.
Якщо система виявила → тоді reconciliation/saga і є «ack» на системному рівні, просто названий інакше.

TLA+ моделює саме це: crash window між StoreResult і CommitOffset. Назва «ack» чи «reconciliation» не важлива — важливо, що між обробкою та підтвердженням є вікно, де crash створює невизначеність.

Мейнтейнер RabbitMQ підтвердив: це фундаментальна властивість at-least-once семантики, не баг реалізації.

Дякую за коментар, цікава думка.
Ваша теза про атомарність івентів вірна на транспортному рівні — так, відправка чи отримання самого івенту є атомарною операцією. Але race condition виникає не «в івенті», а в crash-вікні між отриманням івенту та підтвердженням про його обробку.
Навіть у «чистій» event-driven архітектурі:

1. Consumer отримує івент
2. Обробляє його (змінює свій стан, зберігає в БД, тощо)
3. Відправляє відповідний івент далі
4. Підтверджує отримання (ack/offset commit)

Теоретично ви праві — паттерни справді покривають більшість проблем. Але на практиці навіть досвідчені інженери роблять помилки в crash-вікні між StoreResult і CommitOffset — не тому, що не знають паттерн, а тому що в реальному коді ці паттерни перетинаються з таймаутами, реконектами, і багатошаровими абстракціями бібліотек.
Цінність TLA+ не в тому, щоб замінити «людину з прямими руками». Вона в тому, щоб за 3 секунди довести (математично, а не інтуїтивно), що саме ваш набір паттернів у вашій конфігурації дає гарантію безпеки. Людина перевіряє один сценарій. TLC перевіряє всі можливі переплетіння.
Chaos validation — це не заміна код-рев’ю. Це емпіричне підтвердження, що математична абстракція не збрехала.

Serhii, ви абсолютно праві — at-least-once delivery це свідомий дизайн брокерів, і idempotent consumer це стандартна рекомендація. Стаття не претендує на відкриття цього факту.

Суть issues не в тому, щоб «звалити провину на брокер». Вона в тому, що:
1) Формальний TLA+ доказ робить це знання відтворюваним — не «інтуїтивно зрозуміло», а «доведено для всіх можливих станів».
2) Одна специфікація покриває Kafka, NATS, RabbitMQ — це узагальнення, якого немає в документації жодного з них.
3) Chaos cross-validation підтверджує, що абстрактна модель і реальність збігаються.

Іншими словами, ми не кажемо «брокер зламаний». Ми кажемо: «ось математичний інструмент, який ловить цей клас помилок до деплою, і він працює на будь-якому брокері».

Vitaliy, якщо маєте змістовні заперечення по суті — готовий вислухати. TLA+ і temporal collisions — це досліджена тема (Amazon, Microsoft, researchers). «Студент» і «блохи» — не аргумент.

суть аналогії була в іншому: write skew — це паттерн, де дві «правильні» операції порушують глобальний інваріант через відсутність координації. У Kafka саме це відбувається між двома consumers: кожен окремо успішно виконує StoreResult + CommitOffset, але разом вони можуть продублювати повідомлення. Це структурно той самий клас проблеми, хоча механізм реалізації інший (не СУБД, а розподілена система).

І так, Kafka producer-side idempotency (EOS) не вирішує цю проблему на стороні consumer — саме тому потрібна формальна верифікація на кшталт TLA+, щоб знайти такі переплетення до деплою.

Дякую за питання.

Методологія:
1. Аналізуємо документацію протоколу (не код). Для Kafka — offset commit protocol, для RabbitMQ — AMQP ack, для NATS — JetStream ack.
2. Будуємо TLA+ модель вручну, створюючи абстракцію протоколу: стейт-машина consumer + broker з crash-вікном між StoreResult і CommitOffset/Ack.
3. TLC вичерпно перевіряє всі можливі переплетіння подій (47–8641 станів залежно від конфігурації).
4. Паралельно працюємо над автоматизацією: LLM генерує CRL-граф (Collision Region Language) → TLA+ → TLC → repair loop. Для типових брокерів шаблони вже готові.
5. Chaos validation через Toxiproxy: прогноз TLC підтверджуємо фізичним експериментом (docker kill, network disconnect).

Відмінність від randomized testing: вичерпний пошук, а не випадковий. Гарантія, а не ймовірність.

А якщо тести все ще падають після 40% — значить, треба просто додати ще один рівень абстракції. І більше CS2, звісно.

Справедливо — рішення справді потребує idempotency. Але аналогія з write skew була про структурну схожість: як і в прикладі з лікарями, кожен consumer окремо виконує логічно коректну дію (StoreResult), але через відсутність координації між ними (CommitOffset не синхронізовано з результатом) система в цілому порушує інваріант. Idempotency — це спосіб захисту, а write skew — це клас проблеми.