SymCrypt

בפוסט של מחלקת המחקר של מיקרוסופט (Microsoft Research), נחשף כיצד החברה משתמשת בשפות Rust ו-Lean, בכלי Aeneas ובסוכני בינה מלאכותית (AI Agents) כדי לבצע אימות פורמלי מקיף של אלגוריתמי קריפטוגרפיה בייצור בתוך ספריית SymCrypt. הפרויקט, המשמש ב-Windows וב-Azure, מציג גישה חדשנית המאפשרת לאמת את הקוד בדיוק כפי שנכתב על ידי המפתחים, ללא פגיעה בביצועים או התעלמות מאופטימיזציות חומרה. המאמר מתאר את השלבים מהפיכת תקנים למפרטים פורמליים, דרך תרגום קוד Rust באמצעות Aeneas, ועד לשימוש בסוכני AI לכתיבת הוכחות המאומתות באופן דטרמיניסטי.