Opus'un race condition bulgusuyla TLA+ hype'ı geri döndü; eğitimci dilin neleri kontrol edemediğini anlattı

Formal verification istenmeden spotlight anını yaşıyor. Uzun süredir TLA+ eğitmeni ve savunucusu olan Hillel Wayne'in bir newsletter yazısına göre bunun tetikleyicisi, Claude Code'un mucidi Boris Cherny'nin yakın zamanda Opus'un TLA+ kullanarak koddaki race condition'ları bulabildiği yönündeki açıklamasıydı. Bu iddia çevrimiçi ortamda formal methods hakkında büyük bir tartışma dalgası başlattı ve Hacker News'in ön sayfasına çıkan Wayne'in dengeleyici yazısı, dilin gerçekte neyi kapsadığına dair referans noktası hâline geldi.

Wayne, yıllardır tanıttığı bir araca gösterilen bu ilginin heyecan verici olduğunu, ancak beraberindeki coşkunun kendisini endişelendirdiğini yazıyor. Şu an çevrimiçi dolaşan, formal methods'ın agentic yazılım geliştirme sorununu bir kez ve sonsuza dek çözeceği fikrini kesinlikle reddediyor. Doğrulanmış bir tasarımın otomatik olarak doğru kod üretmediği gibi bilinen uyarıyı tekrarlamak yerine daha ince bir sınıra odaklanıyor: Bir özelliği doğrulayabilmek için önce dilin ifade edebildiği bir özelliğe ihtiyacınız var.

TLA+ neyi kontrol eder

TLA+ bir sistemi davranışlar koleksiyonu olarak modeller; her davranış bir durum dizisidir. Tek bir durum hakkında sıradan boolean ifadeleri — örneğin tüm trafik ışıklarının kırmızı olması — üç temporal operatörle birleşir: biri özelliğin şimdi ve gelecekteki her durumda geçerli olduğunu, biri çok sonraki durumda geçerli olduğunu, biri de şimdi ya da daha sonraki bir noktada geçerli olduğunu ifade eder. Bir always-öelliğini her davranış boyunca kontrol etmek, TLA+ doğrulamasının iş atını oluşturan invariant'ı verir. Next-state operatörlerini bir always içine sarmak, azalmayan bir değer gibi action property'leri üretir. İkisi de safety property'dir — kabaca, kötü bir şeyin hiç olmadığına dair güvenceler. Eventually operatörü üzerine kurulu liveness property'ler ise iyi bir şeyin gerçekleştiğini iddia eder: leader election sonrasında node'ların sonunda anlaşması, bir algoritmanın sonunda doğru sonuçlarla sonlanması ya da bir koşulun sonunda diğerine yol açması gibi. Wayne'e göre invariant'lar, action property'ler, liveness ve refinement, insanların fiilen kontrol ettikleri şeylerin ezici çoğunluğunu oluşturur.

İfade edemediği özellikler

Wayne kör noktaları birkaç gruba ayırıyor.

Birincisi, formalize edemediğiniz her şey. Bir gereksinim mantıksal formül olarak yazılamıyorsa — örneği, bir uygulamanın kuşları tanıdığını kanıtlamaktır — hiçbir formal method yardımcı olamaz.

İkincisi, çok adımlı ve zamanlı iddialar. TLA+ safety property'leri tek durumlar veya tek geçişlerden bahseder; bu yüzden delete'e basıp sonra undo yapmakla orijinal durumun geri geldiğini ya da bir bilgisayarın güç düğmesine basıldıktan sonraki on adım içinde açıldığını doğal biçimde ifade edemezsiniz. Floating-point işlemleri ve gerçek zaman da kapsam dışıdır; mantık yalnızca mantıksal zamanı görür.

Üçüncüsü, reachability. Özellikler tüm davranışlar üzerinden örtük olarak nicellendiğinden, bir davranışın var olduğunu — bir oyunun kazanılabilir olduğunu ya da verilen bir duruma her başlangıçtan ulaşılabilir olduğunu — iddia etmenin yolu yoktur.

Dördüncüsü, davranış kümeleri üzerinden nicellenen hyperproperty'ler. Bir telefonun güç tasarrufu modunun her zaman normal moddan daha az güç çektiğini doğrulamak iki çalıştırmayı karşılaştırmayı gerektirir; tek davranışlı bir mantık bunu ifade edemez. Wayne, birçok güvenlik özelliğinin ve tüm istatistiksel özelliklerin — örneğin 95. persentil yanıt süresinin — bu kovada yer aldığını belirtiyor.

Son olarak, durum uzayının bütününe dair metaproperty'ler — iki durum arasında tam olarak tek yol olması gibi — ancak Wayne bunların pratikte ne kadar yararlı olacağından emin olmadığını itiraf ediyor.

Maliyetli workaround'lar

Bu sınırların hiçbiri mutlak değil. Wayne, iki adımlı özellikleri taklit etmek için durumların geçmişini bir yardımcı değişkende saklamayı ve bazı hyperproperty'leri yaklaşık olarak elde etmek için self-composition'ı — şişirilmiş bir spec'in her davranışının gerçek sistemin iki davranışını paketlemesi — anlatıyor. TLC model checker artık temel reachability soruları için bir REACHABLE anahtar kelimesi ve bazı durum uzayı sorguları için bir TLCGet mekanizması sunuyor; Andrew Helwer ise fairness ve machine closure kullanarak always-reachable davranışı taklit etmeye dair yazılar yazdı.

Ama Wayne tüm bunları hack olarak nitelendiriyor. Her biri kurulması için ciddi bir zekâ gerektiriyor; yardımcı değişkenler refinement'ı bozuyor, self-composition durum uzayını üstel biçimde büyütüyor ve bu teknikler araç setinin geri kalanıyla iyi birleşmiyor.

Neden önemli

Opus gibi agent'lar gerçekten TLA+ kullanabilirse, tasarım düzeyinde doğrulama çok daha erişilebilir hâle gelir ve race condition avı, tam olarak dilin kurulduğu sorun türüdür. Ancak sınır, yetenek kadar önemli. TLA+, mantıksal zamanda, specification düzeyinde, her davranışın özelliği olarak ifade edilebilen şeyleri kontrol eder — ve doğrulanmış bir spec, doğrulanmış kod değildir. Formal methods'ın yapay zekâ tarafından yazılan yazılımın risklerini etkisizleştireceği fikrine ikna olan ekipler bu duvarlara hızla çarpar. Wayne'e göre dürüst söylem daha dar ama daha kalıcı: karmaşık eşzamanlı sistemleri doğru tasarlama konusunda güçlü bir araç — diğer tüm güvence tekniklerinin yerine değil, yanında çalışan.