पिछले सप्ताह, Boris Cherny, Claude Code के आविष्कारक, ने उल्लेख किया कि Opus कोड में रेस कंडीशन खोजने के लिए TLA+ का उपयोग करने में सक्षम था। अब हर कोई औपचारिक सत्यापन के बारे में बात कर रहा है। एक लंबे समय के शिक्षक और TLA+ के समर्थक के रूप में, यह रोमांचक है। लेकिन नया उत्साह मुझे चिंतित करता है। औपचारिक विधियाँ एजेंटिक सॉफ्टवेयर विकास की समस्या को एक बार और हमेशा के लिए हल नहीं करेंगी।

सही डिज़ाइन स्वचालित रूप से सही कोड में परिवर्तित नहीं होते हैं। किसी गुण को सत्यापित करने के लिए, हमें सत्यापित करने के लिए एक गुण की आवश्यकता होती है। TLA+ सिस्टम को व्यवहारों में विभाजित करता है, प्रत्येक राज्यों का एक अनुक्रम है। प्रत्येक राज्य में हम तीन अस्थायी ऑपरेटरों के साथ बूलियन अभिव्यक्ति व्यक्त कर सकते हैं: `[]P` (हमेशा P), `P'` (अगले राज्य में P), और `<>P` (अंततः P)।

`[]P` का अर्थ है कि P प्रत्येक व्यवहार के प्रत्येक राज्य में सत्य है, जिसे अपरिवर्तनीय कहा जाता है। `[](x' >= x)` एक क्रिया गुण है। ये सुरक्षा गुण हैं: कुछ बुरा कभी नहीं होता। जीवंतता गुण `<>` का उपयोग करते हैं: `[]<>P` का अर्थ है कि P प्रत्येक राज्य के कम से कम एक भविष्य के राज्य में सत्य है; `<>[]P` का अर्थ है कि P सत्य हो जाता है और हमेशा सत्य रहता है; `[](P => <>Q)` का अर्थ है कि P अंततः Q का कारण बनता है।