Boris Cherny'nin viral TLA+ paylaşımı: TLA+ aslında neyi doğrular

Boris Cherny bu hafta Claude Agent SDK'nın bazı bölümlerini Opus 5.5 kullanarak TLA+ ve Lean'de modelledi ve paylaşım yaklaşık bir milyon görüntülenme ve binlerce kaydetme aldı, yorumlarda hep aynı soru vardı, TLA+ tam olarak nedir? Araç 30 yılı aşkın süredir var ve pratikte sık görülüyor: Datadog kısa süre önce harness-first ajanları yazdı, formal modeller ise uzun zamandır AWS, MongoDB, Datadog ve Kafka'da kullanılıyor.

TLA+ nedir

TLA+ (Temporal Logic of Actions), iki şeyi yazmak için bir dildir: sistemin neler yapabileceğini anlatan geçiş sistemi ve her çalıştırmada neyin geçerli olacağını anlatan zamansal özellikler. Durumlar anlık görüntülerdir (kim aday, kim kime oy verdi, kim lider), eylemler ise aralarındaki tek adımlardır.

Klasik örnek lider seçimidir: a, b ve c adlı üç bilgisayar tek lider üzerinde anlaşmalıdır ve aynı anda iki lider olamaz. Güvenlik özellikleri kötü hiçbir şeyin olmadığını, canlılık (liveness) özellikleri ise iyi bir şeyin eninde sonunda olacağını söyler, örneğin bir liderin seçilmesini. TLA+'da bunlar üç basit operatörle yazılır: her zaman, eninde sonunda ve leads-to.

Standart denetleyici TLC, sonlu bir modelin erişilebilir tüm durumlarını dolaşır ve bir özellik ihlalinde karşı örnek döndürür. Üç bilgisayarda tüm uzay 38 durumdur; dokuzda ise bir milyonu aşar.

TLA+ ne değildir

Üç uyarı var. Model denetimi yalnızca sonlu durumları kapsar, bu yüzden genel iddia ispat gerektirir; TLA+'nın kendi ispat aracı TLAPS'in otomasyonu, özellikle liveness için sınırlıdır. Spesifikasyon yazılımın ayrı bir modelidir: uygulamanın ona tam uyduğunu hiçbir şey garanti etmez ve kod değiştikçe ikisi uzaklaşabilir. TLA+ doğrusal zamansal mantığa dayandığı için, CTL ve ATL'nin ifade edebildiği alternatif gelecekler veya stratejilere dair özellikler onun kapsamı dışında kalır.

Modellerden makine doğrulamalı ispatlara

Modern ispat sistemleri daha ileri gider. Lean etkileşimli ve geneldir; Boris Cherny'nin paylaşımındaki ispat aracı da oydu. Verus Rust etrafında tasarlandı, spesifikasyonlar ve ispatlar gerçek uygulamanın yanında yaşayabilir. Veil durum makinesi modellerine odaklanır; kısa süre önce bir sync engine doğrulamasında kullanıldı ve 17 hata düzeltildi.

Reasonable ekibi bu yolun bir kısmını otomatikleştiriyor. Kurdukları hattı, 16.459 gerçek TLA+ spesifikasyon-özellik çiftini 3.000'den fazla makine doğrulamalı Verus ispatına dönüştürdü: bir ajan ispatı yazıyor, diğeri inceliyor, bir denetçi ise hiçbirinin spesifikasyonu değiştirmediğini ve assume(false) gibi kısa yollara başvurmadığını kontrol ediyor. Hedef, tek bir döngüde tanımlanan, uygulanan ve doğrulanan yazılım.