গত সপ্তাহে, 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 ঘটায়।