Claude Opus 5.5, Agent SDK'yi TLA+ ile modelledi ve formal yöntemler trend oldu

Bu hafta Boris Cherny, Claude'un Opus 5.5'inden Claude Agent SDK'nin bölümlerini TLA+ ve Lean ile modellemesini istemesinin sonuçlarını paylaştı. Konuyu ele alan takip yazısıyla Hacker News'in ana sayfasına ulaşan Reasonable'a göre tweet yaklaşık bir milyon görüntüleme ve binlerce yer imi aldı ve geniş bir kitleyi temel bir soru sormaya itti: TLA+ nedir?

TLA+ nedir

TLA+, Temporal Logic of Actions'ın kısaltması, otuz yılı aşkın süredir var olan bir formal modelleme dilidir. Reasonable'ın açıkladığı gibi, bir TLA+ modeli iki şeyi tanımlar: bir geçiş sistemi, yani bir sistemin bulunabileceği durumlar ve bunlar arasında geçişi sağlayan tek adımlar; ve zamansal özellikler, yani bir çalışmanın zaman içinde nasıl geliştiğine dair iddialar.

Reasonable'ın örnek olarak kullandığı senaryo, aynı anda iki liderin asla var olmaması gereksinimiyle üç bilgisayar arasında yapılan bir lider seçimidir. TLA+ geçişlere kasıtlı olarak herhangi bir sıralama getirmez ve farklı olayların olasılıklarını modellemez; Reasonable buna, mesajların, zaman aşımlarının ve kullanıcı eylemlerinin birçok farklı sırada iç içe geçebildiği dağıtık sistemler için doğru soyutlama diyor.

Özellikler iki çeşittir. Safety hiç kötü şeyin yaşanmamasını, liveness ise iyi bir şeyin sonuçta gerçekleşmesini söyler. Reasonable, sonsuza dek boşta duran bir sistemin mükemmel şekilde güvenli olduğuna dikkat çeker; liveness'ın bu yüzden önemli olduğunu ve adil olma (fairness) varsayımlarına — örneğin sürekli etkin kalan bir eylemin sonuçta mutlaka gerçekleştirilmesi gerektiği gibi — ihtiyaç duyduğunu belirtir.

Standart model denetleyici TLC, bu özellikleri sonlu bir örneğin erişilebilir her durumunu tek tek inceleyerek doğrular. Üç bilgisayar için bu 38 durum anlamına gelir ve denetleyici iki liderin asla bir arada olmadığını teyit eder. Bir kuralı, bir bilgisayarın iki kez oy verebileceği şekilde değiştirin, TLC iki liderle biten altı adımlı bir karşı örnek döndürür. Dokuz bilgisayarda durum uzayı bir milyonu aşar; bu da aracın temel sınırlamasının bir ön görüntüsüdür.

TLA+'ın tükendiği üç nokta

Reasonable, bir TLA+ modelinin tam kapsamlı yazılım doğrulaması olmadığını açıkça söylüyor ve üç boşluk listeliyor.

Birincisi, model denetimi yalnızca sonlu örnekleri kapsar. Bir özelliği rastgele sistem boyutları için ortaya koymak bir kanıt gerektirir ve TLA+'ın kendi kanıtlayıcısı TLAPS, özellikle liveness argümanları konusunda sınırlı otomasyona sahiptir.

İkincisi, model uygulamanın kendisi değildir. Kodun şartnameye uygun davrandığını otomatik olarak garanti eden bir şey yoktur ve ikisi, kod değiştikçe birbirinden uzaklaşabilir; bu, klasik şartname-uygulama boşluğudur.

Üçüncüsü, ifade gücü. TLA+, tekil çalışmalar hakkında iddialar ileri süren doğrusal zamansal mantığa dayanır. CTL gibi dallanan-zaman mantıkları herhangi bir durumdan yeni bir seçimin hâlâ başlatılabileceğini söyleyebilir; ATL gibi stratejik mantıklar ise bir bilgisayarın, diğerleri ne yaparsa yapsın, lider olmak için bir stratejiye sahip olduğunu söyleyebilir — bir sistem çok sayıda etkileşen agent içerdiğinde anlam kazanan türden bir özellik.

Bunların hiçbiri benimsenmeyi engellemedi. Reasonable, TLA+'ın AWS, MongoDB ve Datadog'da ve Kafka'nın içinde kullanıldığını, Datadog'un ise TLA+'ın agent destekli kodlamada karşılığını verdiğine dair erken bir işaret olarak harness-first agent'lar üzerine yayın yaptığını belirtiyor. Jack Vanlightly da TLA+'ı, agent'lar bunu moda hale getirmeden çok önce blogunda öğretiyor.

Şartnamelerden kanıtlara ve koda

Bu sınırların ötesine geçen yol modern kanıt sistemlerinden geçiyor; Reasonable bunlardan üçünü öne çıkarıyor. Cherny'nin gönderisinde kullanılan kanıtlayıcı Lean, etkileşimli ve genel amaçlıdır. Verus, Rust etrafında kurulmuştur; böylece şartnameler, kanıtlar ve gerçek uygulama tek bir dilde yaşar — bu, şartname-uygulama boşluğuna doğrudan bir saldırıdır. Leo de Moura'nın önerdiği, durum makinesi modelleri için Lean tabanlı bir araç olan Veil ise yakın zamanda bir sync engine'i doğrulamak için kullanıldı ve bu süreçte 17 hata düzeltti; ancak liveness hâlâ gelecek çalışma konusu ve doğrulanmış model uygulamadan ayrı durumda.

Zaten yapay zekâ da bu hat içine giriyor. Reasonable, 16.000'den fazla TLA+ şartname ve özellik çiftini 3.000'i aşkın makine tarafından doğrulanmış Verus kanıtına dönüştüren agent tabanlı bir pipeline kurduğunu söylüyor; bu da modelden kanıta giden yolun bir bölümünün artık otomatikleştirilebileceğinin kanıtı.

Neden önemli

Viral tweet bir belirti, asıl hikâye değil. Agent'ların yazdığı şartnameler ancak onları denetleyen bir şey varsa önem taşır ve Reasonable'ın ortaya koyduğu soru, bir agent'ın TLA+ yazıp yazamayacağı değil, agent'lar şartnameler, kanıtlar ve gerçek programlar arasında akıcı biçimde hareket ettiklerinde nelerin mümkün olacağıdır. Formal yöntimler her zaman maliyet yüzünden tıkanmıştır: durum uzayı patlaması, elle yapılan kanıtlar ve tanımladıkları koddan uzaklaşan modeller. Agent'lar şartnameleri, uygulamanın kendisine bağlı makine tarafından doğrulanmış kanıtlara rutin biçimde çevirebilirse, doğrulama veritabanı iç yapılarına ayrılmış bir uzmanlık faaliyeti olmaktan çıkar ve sıradan agent destekli geliştirmenin bir parçası haline gelir. İnce sıralama ve yeniden deneme hatalarının norm olduğu agent harness'leri inşa eden ekipler için bu değişimin muhtemelen ilk olarak orada ortaya çıkması beklenir.