Boris Çerninin viral TLA+ tviti: formal model əslində nəyi yoxlayır

Bu həftə Boris Çerni Opus 5.5 ilə Claude Agent SDK-nın hissələrini TLA+ və Lean-də modelləşdirdi və paylaşım təxminən bir milyon baxış və minlərlə yadda saxlama topladı, şərhlərdə isə eyni sual səslənirdi, TLA+ tam olaraq nədir? Alət 30 ildən çoxdur ki mövcuddur və praktikada tez-tez görünür: Datadog bu yaxınlarda harness-first agentlər barədə yazdı, formal modellər isə uzun müddətdir AWS, MongoDB, Datadog və Kafka-da istifadə olunur.

TLA+ nədir

TLA+ (Temporal Logic of Actions) iki şeyi yazmaq üçün dildir: sistemin nə edə biləcəyini təsvir edən keçid sistemi və hər icrada nəyin doğru olmalı olduğunu bildirən zaman xassələri. Vəziyyətlər anlıq görüntülərdir (kim namizəddir, kim kimə səs verib, kim liderdir), hərəkətlər isə aralarındakı ayrı addımlardır.

Klassik nümunə lider seçimidir: üç kompüter, a, b və c, bir lider üzərində razılaşmalıdır və eyni anda iki lider ola bilməz. Təhlükəsizlik xassələri pis heç nəyin baş vermədiyini, liveness xassələri isə yaxşı bir şeyin nəhayət baş verəcəyini deyir, məsələn liderin seçilməsini. TLA+-da bunlar üç sadə operatorla yazılır: həmişə, nəhayət və leads-to.

Standart yoxlayıcı TLC sonlu modelin bütün əlçatan vəziyyətlərini araşdırır və xassə pozulanda əks-nümunə qaytarır. Üç kompüter üçün bütün məkan 38 vəziyyətdir, doqquz üçün isə milyonu keçir.

TLA+ nə deyil

Üç xəbərdarlıq var. Model yoxlaması yalnız sonlu halları əhatə edir, ona görə ümumi iddia sübut tələb edir; TLA+-ın öz sübutedici aləti TLAPS-in avtomatlaşdırması isə, xüsusən liveness üçün, məhduddur. Spesifikasiya proqramın ayrı modelidir: tətbiqin ona tam uyğun davrandığına heç nə zəmanət vermir və kod dəyişdikcə ikisi uzaqlaşa bilər. TLA+ xətti zaman məntiqinə əsaslandığı üçün CTL və ATL-in ifadə edə bildiyi alternativ gələcəklər və ya strategiyalar barədə xassələr onun imkanlarından kənarda qalır.

Modellərdən maşınla yoxlanılan sübutlara

Müasir sübut sistemləri daha irəli gedir. Lean interaktiv və ümumidir; Boris Çerninin paylaşımındakı sübutedici də o idi. Verus Rust ətrafında qurulub, ona görə spesifikasiyalar və sübutlar real tətbiqin yanında yaşaya bilər. Veil vəziyyət maşını modellərinə yönəlib və bu yaxınlarda sync engine-in yoxlanması üçün istifadə edildi, bu zaman 17 səhv düzəldildi.

Reasonable komandası bu yolun bir hissəsini avtomatlaşdırır. Onların boru xətti 16 459 real TLA+ spesifikasiya-xassə cütünü 3 000-dən çox maşınla yoxlanılan Verus sübutuna çevirdi: bir agent sübut yazır, digəri yoxlayır, ayrı nəzarətçi isə heç birinin spesifikasiyanı dəyişmədiyini və assume(false) kimi qısa yollara əl atmadığını yoxlayır. Məqsəd bir dövrdə təsvir olunan, yazılan və yoxlanılan proqram təminatıdır.