Boris Cherny-ს ტვიტი TLA+-ზე: რას ამოწმებს ფორმალური მოდელი

ამ კვირაში Boris Cherny-მ Opus 5.5-ით Claude Agent SDK-ის ნაწილები TLA+-სა და Lean-ში აღწერა, პოსტმა დაახლოებით მილიონი ნახვა და ათასობით შენახვა მოაგროვა, კომენტარებში კი ერთი და იგივე კითხვა გაისმოდა, რა არის TLA+. ეს ხელსაწყო 30 წელზე მეტია არსებობს და პრაქტიკაში ხშირად ჩანს: Datadog-მა ცოტა ხნის წინ harness-first აგენტებზე დაწერა, ფორმალურ მოდელებს კი დიდი ხანია AWS-ში, MongoDB-სა და Kafka-ში იყენებენ.

რა არის TLA+

TLA+ (Temporal Logic of Actions) ორ რამეს აღწერს: გადასვლების სისტემას, ანუ იმას, რისი გაკეთებაც სისტემას შეუძლია, და დროით თვისებებს, ანუ იმას, რა უნდა სრულდებოდეს ყველა გაშვებაში. მდგომარეობები კადრებია (ვინ არის კანდიდატი, ვის მისცა ხმა, ვინ გახდა ლიდერი), მოქმედებები კი მათ შორის გადადგმული ერთი ნაბიჯია.

კლასიკური მაგალითია ლიდერის არჩევა: სამი კომპიუტერი, a, b და c, ერთ ლიდერზე უნდა შეთანხმდეს და ერთდროულად ორი ლიდერი არ უნდა არსებობდეს. უსაფრთხოების თვისებები ამბობენ, რომ ცუდი არასოდეს ხდება, liveness-ის თვისებები კი, რომ კარგი მოვლენა საბოლოოდ მოხდება, მაგალითად ლიდერი აირჩევა. TLA+-ში ამას სამი მარტივი ოპერატორით წერენ: ყოველთვის, საბოლოოდ და leads-to.

TLC, სტანდარტული მოდელის შემმოწმებელი, სასრული მოდელის ყველა მიღწევად მდგომარეობას ამოწმებს და თვისების დარღვევისას კონტრმაგალითს აბრუნებს. სამი კომპიუტერისთვის მთელი სივრცე 38 მდგომარეობაა, ცხრისთვის კი მილიონს სცდება.

რა არ არის TLA+

სამი რამ უნდა გავითვალისწინოთ. მოდელის შემოწმება მხოლოდ სასრულ შემთხვევებს მოიცავს, ამიტომ ზოგადი მტკიცება მტკიცებას მოითხოვს, TLA+-ის საკუთარი პროვერის, TLAPS-ის ავტომატიზაცია კი შეზღუდულია, განსაკუთრებით liveness-ისთვის. სპეციფიკაცია პროგრამის ცალკე მოდელია: ვერაფერი იძლევა გარანტიას, რომ იმპლემენტაცია ზუსტად მას მიჰყვება, და კოდთან ერთად ისინი შეიძლება დაშორდნენ. TLA+ წრფივ დროით ლოგიკას ეყრდნობა, ამიტომ ალტერნატიულ მომავალზე ან სტრატეგიებზე საუბარი, რასაც CTL და ATL ახერხებენ, მის ფარგლებს სცდება.

მოდელიდან მანქანურად შემოწმებულ მტკიცებამდე

თანამედროვე პროვერები უფრო შორს მიდიან. Lean ინტერაქციული და ზოგადია, და სწორედ ის გამოიყენა Boris Cherny-მ თავის პოსტში; Verus Rust-ის გარშემოა აგებული, ამიტომ სპეციფიკაცია და მტკიცება რეალური იმპლემენტაციის გვერდით შეიძლება იცხოვროს; Veil მდგომარეობათა მანქანების მოდელებზეა მორგებული და ცოტა ხნის წინ sync engine-ის შესამოწმებლად გამოიყენეს, რის დროსაც 17 შეცდომა გამოსწორდა.

Reasonable-ის გუნდი ამ გზის ნაწილს ავტომატიზებს. მათი პაიპლაინი 16 459 რეალურ TLA+ წყვილს 3 000-ზე მეტ მანქანურად შემოწმებულ Verus-ის მტკიცებად აქცევს: ერთი აგენტი მტკიცებას წერს, მეორე ამოწმებს, ცალკე გუშაგი კი აკონტროლებს, რომ არცერთს სპეციფიკაცია არ შეუცვლია და assume(false)-ის მსგავსი მოკლე გზა არ გამოუყენებია. მიზანია პროგრამა, რომელიც ერთ ციკლშია აღწერილი, დაწერილი და შემოწმებული.