אימות פורמלי הוא הוכחה מתמטית שקוד עושה בדיוק את מה שהוגדר לו. הוא נחשב לרמת הבטחת האבטחה הגבוהה ביותר, אבל דורש עבודה ידנית רבה. ב-AlphaProof Code, לפי דיפמיינד, מומחים מחליטים יחד עם מודלים מה צריך להוכיח, וקבוצת סוכני AI שמבוססים על Gemini Carbon כותבת את ההוכחות בשפת Lean, שבודקת כל הוכחה אוטומטית. בסוף הסוכנים סימנו לבדיקה אנושית רק כאחוז אחד מהקוד.
החברה בחרה בפרוטוקול Signal, שמצפין שיחות באפליקציית Signal וב-Google Messages. לדבריה, זו הפעם הראשונה ש-AI מאמת פורמלית פרוטוקול קריפטוגרפי בשימוש נרחב לעומק כזה, והפעם הראשונה שהמימוש של פרוטוקול כזה אומת בכלל, בכל שיטה. ההוכחות מכסות תכונות כמו הגנה על הודעות לפני ואחרי פריצה זמנית למכשיר, ומגיעות עד הקוד המהודר. העבודה נמשכה ארבעה שבועות; לדברי דיפמיינד, בעבר משימה כזו לקחה לצוותי מומחים שנים.
כדי לבדוק שהמערכת מבחינה בין קוד תקין לפגום, החוקרים החזירו לגרסה מבודדת של הקוד שני באגים אמיתיים שתוקנו בעבר, ובשני המקרים התקבלה הוכחה ממוחשבת שהגרסה הפגומה אינה מאובטחת. ה-CTO של Signal, אהרן קרט, אמר שתרגום של קוד חי למשפטים תקפים ב-Lean בעזרת סוכני AI הוא פריצת דרך משמעותית. דיפמיינד מפרסמת את חומרי האימות בקוד פתוח יחד עם מאמר טכני, ואומרת שהרחבת השיטה למערכות נוספות תדרוש עוד מחקר.