Вірусний твіт Боріса Черні про TLA+: що насправді перевіряє формальна модель

Цього тижня Боріс Черні за допомогою Opus 5.5 змоделював частини Claude Agent SDK мовами TLA+ та Lean, допис зібрав близько мільйона переглядів та тисячі збережень, а в коментарях лунало те саме питання, що таке TLA+. Цьому інструменту понад 30 років, і він частіше трапляється на практиці: нещодавно Datadog написала про агентів у стилі harness-first, а формальні моделі давно використовують в AWS, MongoDB, Datadog і Kafka.

Що таке TLA+

TLA+ (Temporal Logic of Actions) — мова для опису двох речей: системи переходів, тобто того, що система може робити, і темпоральних властивостей, тобто того, що має виконуватися в кожному запуску. Стани — це знімки (хто кандидат, хто за кого голосував, хто лідер), а дії — окремі кроки між ними.

Класичний приклад — вибір лідера: три комп'ютери, a, b і c, мають домовитися про одного лідера, і двох лідерів одночасно бути не може. Властивості безпеки кажуть, що погане ніколи не стається; властивості живучості (liveness) — що добре рано чи пізно станеться, наприклад лідера буде обрано. У TLA+ це записують трьома простими операторами: завжди, зрештою та leads-to.

TLC, стандартний перевіряльник моделей, досліджує кожен досяжний стан скінченної моделі й повертає контрприклад, коли властивість порушується. Для трьох комп'ютерів увесь простір — 38 станів, для дев'яти він перевищує мільйон.

Чим TLA+ не є

Є три застереження. Перевірка моделей працює зі скінченними випадками, тож загальне твердження потребує доведення, а власний доводжувач TLA+, TLAPS, має обмежену автоматизацію, особливо для liveness. Специфікація — це окрема модель програми: ніщо не гарантує, що реалізація поводиться так само, і зі змінами коду вони можуть розійтися. І оскільки TLA+ побудований на лінійній темпоральній логіці, властивості про альтернативні майбутні або стратегії, які вміють виражати CTL та ATL, для нього недосяжні.

Від моделей до машинно-перевірених доведень

Сучасні системи доведення йдуть далі. Lean — інтерактивний і загальний, саме його використали в дописі Черні; Verus створений навколо Rust, тож специфікації та доведення можуть жити поруч із реальною реалізацією; Veil орієнтований на моделі скінченних автоматів і нещодавно допоміг перевірити sync engine, виправивши 17 помилок.

Команда Reasonable автоматизує частину цього шляху. Їхній пайплайн перетворив 16 459 реальних пар «специфікація + властивість» TLA+ на понад 3 000 машинно-перевірених доведень Verus: один агент пише доведення, другий його перевіряє, а контролер стежить, щоб ніхто не змінив специфікацію і не вдався до скорочень на кшталт assume(false). Мета — програмне забезпечення, яке описують, реалізують і перевіряють в одному циклі.