הציוץ הוויראלי של בוריס צ'רני על TLA+: מה באמת בודק מודל פורמלי

השבוע השתמש בוריס צ'רני ב-Opus 5.5 כדי למדל חלקים מ-Claude Agent SDK בשפות TLA+ ו-Lean, והאינטרנט עשה את שלו: הציוץ צבר כמיליון צפיות ואלפי שמירות, ובתגובות חזרה אותה שאלה, מהו בעצם TLA+. הכלי הזה בן יותר מ-30 שנה, והוא מופיע שוב ושוב בפועל: לאחרונה כתבה Datadog על סוכנים בסגנון harness-first, ומודלים פורמליים משמשים מזה זמן רב ב-AWS, ב-MongoDB, ב-Datadog וב-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). המטרה היא תוכנה שמתוקננת, ממומשת ומאומתת בלופ אחד.