הקוד של AlphaProof הוכיח שהקריפטוגרפיה של Signal נכונה — ברמת הבינארי המקומפל

Six and a half million lines of Lean, produced in four weeks, by agent teams that no human helped write. That is the headline number G​oogle DeepMind published on 10 November 2026 for AlphaProof Code, an agentic framework for formal verification that the lab used to machine-check the cryptographic core of the Signal protocol — and, unusually, to check it at the level of the compiled AArch64 binary rather than the design document above it. The models that did the work are a different question. one API key at provider list price with 0% markup The proof agents' engine is not something we serve.

The framework is not a model you can call. It is a harness: human experts decide what must be true, a mixture of models turns those goals into Lean specifications, and then teams of proof-writing agents — the blog names G​emini Carbon as the engine — fill in the proofs until Lean's kernel accepts them. What shipped alongside the announcement is the artifact set, at github.com/google-deepmind/code-verification, and a technical paper that is far more candid about the boundaries of the result than the blog post is. Most of what follows comes from that paper, because the paper is where the interesting numbers live.

מה למעשה הוכח, וכנגד מה

המטרה היא libsignal v0.105.4 עם spqr v1.6.0, שנבנו באמצעות rustc 1.98.1 הסטנדרטי, מקושרים סטטית ל-musl, ומופקים כקובץ הרצה יחיד של AArch64 Linux. הפרט הזה חשוב יותר מכל benchmark: ההוכחות עוסקות בביתים שירוצו על טלפון, ולא בפונקציית Rust שסומכים על המהדר שיתרגם אותה בנאמנות. הצוות אימת כ-560 KB מקוד המקור של libsignal, כ-140,000 הוראות AArch64, ועשה זאת על ידי כתיבת מודל Lean של סט ההוראות — 467 הוראות ו-31 קריאות מערכת, ב-7,578 שורות — ולאחר מכן הוכיח שתמונת ה-ELF האמיתית, כשהיא נטענת ומבוצעת תחת המודל הזה, משמרת את תכונות האבטחה.

התכונות הן אלו שמהנדס פרוטוקולים היה מבקש. עשרה משפטים סימבוליים מכסים סודיות קדימה, אבטחה לאחר פגיעה, סודיות יוזם ומשיב, אימות, וחמש מסקנות ממשפט 1 של PQXDH. התוצאה העיקרית נקראת signal_session_secure_placed. קיים גם מסלול חישובי עם חסם קונקרטי, ושני המסלולים משתמשים במודלי יריב שונים: הצד הסימבולי (Dolev–Yao, דרך מסגרת DyLean) מכסה אפילו תוקף קוונטי ששובר את Diffie–Hellman לאחר לחיצת היד, בעוד הצד החישובי מכסה יריבים קלאסיים בלבד.

לאן הולכות ששת מיליון השורות

"מעל שישה מיליון שורות" הוא הניסוח של הבלוג, והוא מדויק אך גס. הפירוט במאמר הוא השימושי, וכדאי לקרוא אותו כטבלת עלויות ולא כהתרברבות:

• הוכחות עבור הבינארי — 5.3 מיליון שורות, עיקר העבודה, המכסות את הסמנטיקה של קוד המכונה ואת העידון מהמודל הסמלי עד לקובץ ההרצה.

• הוכחות חישוביות — כ-860,000 שורות.

• הוכחות סמליות — כ־350,000 שורות.

• הוכחות להפרכת באגים — כ-140,000 שורות, עבור שתי הפגיעויות שהוחזרו במכוון המתוארות להלן.

• הוכחות מקצה — כ-70,000 שורות.

כמעט שבעה מיליון שורות אם סופרים הערות ושורות ריקות, מה שהמאמר עושה והבלוג לא. כך או כך, היחס החשוב הוא בין ההוכחה לבין הדבר המוכח: 6.5 מיליון שורות של Lean כדי לבסס תכונות של קובץ בינארי בגודל 560 KB. היחס הזה הוא המדד הכנה לכמה הטכניקה הזו רחוקה מלהיות שגרה, וזה המספר שכדאי לצטט כשמישהו שואל אם אימות פורמלי הפך לזול.

בסיס האמון קטן מההוכחה, וזו הנקודה.

הוכחה שווה רק כפי ששווים ההנחות שעליהן היא נשענת. המאמר מפרט זאת במדויק, והדיוק הוא מה שמבדיל אותו מהודעה לעיתונות. המפרטים הנסמכים הם באורך של כ-18,000 שורות (28,000 עם תיעוד), הסמנטיקה של AArch64 באורך של כ-8,000, וקידוד ה-Lean של קוד המכונה באורך של כ-95,000. שלושים ושבע שגרות מוחלפות בחוזים במקום להיות מאומתות — דחיסת SHA-256 ו-SHA-512, AES-256-CBC, X25519, פעולות עקומת Edwards, Kyber1024 ו-ML-KEM-768, ו-HMAC של libcrux. שמונה עשרה נקודות כניסה של panic מונחות אף הן במקום להיות מוכחות.

אז הטענה אינה ש"הכול מוכח". הטענה היא שלוגיקת פרוטוקול ההצפנה, מכונת מצב הסשן, והעידון מאותה לוגיקה להוראות שבפועל מבוצעות — כל אלה מוכחים, בעוד שהפרימיטיבים שמתחתיהם נחשבים מהימנים כפי שכל פרויקט אימות סומך על הפרימיטיבים שלו. מהדר ה-Rust, באופן בולט, הוא לא בבסיס האמון — הצוות נמנע מהצורך לסמוך עליו באמצעות הסקה ברמת קוד המכונה, וזו אותה תחבולה שמאפשרת להם לעקוף לגמרי מהדר מאומת. לשם הקשר בקנה מידה, המאמר מציין את seL4 בכ-20 שנות אדם ואת CompCert בכ-6.

שני באגים, הוחזרו בכוונה

מערכת אימות שתמיד רק אומרת "נכון" אינה ניתנת לבדיקה. לכן הצוות לקח שתי פגיעויות שכבר נמצאו ותוקנו בעבר בקוד של Signal — באג של מצב חלש ובאג של תת-קבוצה קטנה — והחזיר אותן לעותק מבודד, והריץ מחדש את צינור העיבוד. בשני המקרים AlphaProof Code הפיק הוכחה שנבדקת על ידי מכונה לכך שהגרסה הפגומה נכשלת במשפט האבטחה: ההצהרה הסמלית מצטמצמת ל-¬Sec(Asm_bug).

המאמר מוסיף הסתייגות שדף שיווקי היה משמיט: להפריך את המשפט החישובי עבור אותם באגים הוא "הרבה יותר קשה" והושאר פתוח. במילים אחרות, הבדיקה השלילית עובדת היטב במסלול הסמלי ואינה עובדת עדיין במסלול החישובי. זה בדיוק סוג האסימטריה שכדאי לקורא לדעת עליה לפני שהוא מתייחס למסגרת כאל גלאי באגים.

כיצד הורצו הסוכנים

חמישה חוקרים במשך ארבעה שבועות, כשכל אחד מהם מריץ סוכנים ללא הפסקה. כתיבת ההוכחות עצמה נעשתה על ידי צוותים של 40 עד 80 סוכנים, שפעלו בין 24 ל־72 שעות על מכונה אחת לכל צוות, עם סוכן מפקח מעל מתזמר הצוות. סוכן שומר סף בודק כל הגשה עם משווה מול עותק שמור בצד של המפרט ומול ליבת Lean — הגנה מפני סוכן שמוכיח גרסה מוחלשת במעט של מה שהתבקש.

העבודה האנושית רוכזה בשלב מוקדם על מפרטים. כל מפרט נבדק על ידי מומחה לפני תחילת עבודת ההוכחה, ומעבר הביקורת של הסוכנים עצמם סימן כ־1% מבסיס הקוד לתשומת לב אנושית. אף אדם לא כתב קוד הוכחה. המאמר גם גלוי לב בנוגע להיבט ההנדסי: בנייה נקייה יכולה להימשך כמה שעות, בתחילת הדרך עריכה קטנה בקוד המקור או קובץ בינארי שהודר מחדש אילצו תיקוני הוכחה גדולים, ויש "מרחב משמעותי לאופטימיזציה" הן בהוכחות שנוצרו על ידי AI והן בטכניקות ההוכחה עצמן.

מה שההוכחות אינן מכסות

המגבלות ארוכות מספיק כדי להיות החלק החשוב ביותר במאמר, והן מנוסחות בפשטות. לא נקבעה הבטחה פוסט-קוונטית לתכונת הריפוי של SPQR — משפטי הרצ'ט מניחים שהתוקף בוחר את מפתחות SPQR. פרטיות המטען אינה מוכחת. אימות המשיב אינו מוכח עבור ההודעה הראשונה של לחיצת יד שלעולם אינה מקודמת. המודל מתיר סשן אחד לכל קידום, אורכי הודעות קבועים, ללא מצב ריבוי-מכשירים, ומפתחות זהות של אמון בשימוש ראשון.

קיים גם חסם שהופך לחסר משמעות. איבר זיוף ה-MAC בגודל 8 בתים הוא לפחות 2⁻⁶⁴ לכל ניסיון, וגדל באופן ריבועי במספר ההודעות והאפוקות, מה שאומר שהחסם מפסיק לומר דבר עבור סשן בודד של כ-25,000 הודעות, או עבור 2²⁰ סשנים של 2¹⁰ הודעות. ונושא ההוכחה הוא ה-build של הצוות של libsignal-cli שרץ כתהליך חדש — ולא אפליקציית Signal בטלפון שלך. כמה הנחות סביבה מוצגות באופן לא פורמלי במקום להיות מוכחות.

אין API, אין מחיר, ואין מודל שאפשר לקרוא לו.

זה החלק שיאכזב כל מי שמגיע מלוח דירוג של מודלים. AlphaProof Code הוא מסגרת מחקר ומערך ארטיפקטים שפורסם. אין נקודת קצה, אין מחירון לפי טוקן, אין רשימת המתנה ואין משקולות: המאגר מכיל את פיתוח ה-Lean, את הסמנטיקה של AArch64, את כריכת ה-libsignal ואת המפרטים, ולא צ'ק פוינט. הבלוג אומר שהארטיפקטים בקוד פתוח; דף הנחיתה אינו מציין רישיון, וזה שווה לבדיקה לפני שמישהו מתכנן לבנות על זה.

The models that did the work are a different question. The paper names G​emini 4 Carbon for the proof agents and says Claude Opus 5.5 was used alongside other models for drafting and reviewing specifications. Claude Opus 5.5 is on OrcaRouter's catalogue today at $4 per million input tokens and $20 per million output, with provider list price passed through at 0% markup — so if the practical takeaway you want is "run a spec-drafting loop with the model the paper used," that part is a normal API call, and a vendor price change lands on our side the same day. The proof agents' engine is not something we serve, and nothing here implies we host AlphaProof Code itself.

למה זה עניין גדול יותר מתוצאת Signal

האימות של Signal מרשים במונחים שלו — האימות הפורמלי הראשון, בכל שיטה, עם או בלי AI, לפי DeepMind, שלהיישום של פרוטוקול פרוס באופן נרחב, והפעם הראשונה ש-AI אימת פרוטוקול קריפטוגרפי פרוס בעומק כזה. אבל הטענה שאפשר להעביר הלאה היא זרימת העבודה. צוות של חמישה, בארבעה שבועות, עם שלב של סקירת מפרט ועם סוכן בתפקיד שומר סף, הפיק מאגר הוכחות שפעם היה פרויקט של שנים רבות. אם היחס הזה מחזיק אפילו בקירוב, מערך המערכות שיכולות להרשות לעצמן אימות משתנה: קושחה של מכשירים רפואיים, תוכנה של רשת החשמל, מסוג הקוד שזוכה כיום לסקירת קוד ותפילה.

האם זה מחזיק מעמד טרם נבדק. ההצפנה של Signal מוגדרת היטב באופן יוצא דופן, הצוות הביא מהנדסים של Signal עצמה לסקור את המתודולוגיה, והפרימיטיבים הוזמנו במיקור חוץ במקום שאומתו. המערכת הבאה לא תהיה כה נוחה. המסגור של המאמר עצמו — לצמד אימות פורמלי עם סוכני הגנה אוטומטיים כמו CodeMender — הוא הצורה הכנה של ההצעה: האימות אומר לך מה נכון, ומשהו אחר חייב לתקן את מה שאינו.

מה לראות

Three things would move this from a landmark paper to an industrial technique. A second, independent codebase verified by someone outside G​oogle, ideally one where the specification had to be written from scratch rather than adapted from an existing analysis. A cost figure — agent-hours, accelerator-hours, dollars — because four weeks and 40-to-80-agent teams is not a unit any engineering manager can budget against. And the computational-track bug refutation, which the paper leaves open and which is the difference between a system that proves properties and a system that can also tell you, computationally, that a specific binary is broken.

עד אז, קראו את מאגר הארטיפקטים ולא את ההודעה. ההוכחות נמצאות שם, Lean בודקת אותן, והמאמר אומר לכם בדיוק מה הן מניחות.