Բորիս Չեռնիի վիրուսային թվիթը TLA+-ի մասին. ինչ է իրականում ստուգում ֆորմալ մոդելը

Այս շաբաթ Բորիս Չեռնին 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-ը ինտերակտիվ է և ընդհանուր, հենց այն էլ օգտագործվել է Բորիս Չեռնիի գրառման մեջ. Verus-ը կառուցված է Rust-ի շուրջ, ուստի սպեցիֆիկացիաներն ու ապացույցները կարող են ապրել իրականացման կողքին. Veil-ը նախատեսված է վիճակների մեքենաների համար և վերջերս օգտագործվեց sync engine-ի ստուգմանը՝ ուղղելով 17 սխալ։

Reasonable-ի թիմն ավտոմատացնում է այս ուղին։ Նրանց փայփլայնը 16 459 TLA+ զույգերից կառուցել է ավելի քան 3 000 մեքենայական ստուգված Verus ապացույց. մեկ գործակալ գրում է ապացույցը, մյուսը ստուգում, պահակը հետևում է, որ ոչ ոք չփոխի սպեցիֆիկացիան ու չօգտագործի assume(false)-ի նման կարճ ուղիներ։ Նպատակը մեկ ցիկլում նկարագրվող, իրականացվող ու ստուգվող ծրագիրն է։