מיקרוסופט מדגימה אימות פורמלי לקוד שכתבו סוכני AI עם PDD Kit

סוכן AI יכול לכתוב מנגנון התחברות, אבל מי מוודא שהקוד באמת מקיים את כללי הגישה שהמפתחים התכוונו אליהם? ב־5 בנובמבר 2026 פרסמה Microsoft Research הדגמה של PDD Kit, שמתרגם דרישות למפרט פורמלי ומשתמש ב־Verus כדי לבדוק את הקוד מולו. זו דרך להוסיף הוכחה מתמטית לבדיקת תכונות מוגדרות בקוד, לא אישור שהאפליקציה כולה בטוחה או נטולת תקלות.

01מה הודגם: מדרישות מפתחים למפרט שאפשר לבדוק

ההדגמה מתמקדת במנגנון ההתחברות של אפליקציית Rust שקוד שלה נכתב בידי סוכני AI. במקום להסתפק בשאלה אם מסלול התחברות מסוים עובד בניסוי, PDD Kit מתרגם את דרישות המפתחים למפרט פורמלי. Verus משמש לבדיקת ההתאמה בין הקוד לבין המפרט הזה. מוקד הסיפור הוא לכן לא עוד יכולת לייצר קוד, אלא הדרך לבחון את התוצאה מול תנאים מפורשים.

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

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

02מה הוכחה מוסיפה מעבר לבדיקות רגילות

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

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

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

03גבולות ההוכחה: מי בודק את הדרישה עצמה?

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

גם לסביבת ההפעלה יש משמעות. לצורך המחשה, אפליקציה עשויה לכלול שירות חיצוני, תצורת פריסה או תהליך תפעולי שאינם חלק מהמודל שנבדק. אין לייחס להם את ההבטחה שניתנה לקוד אחר. אלה דוגמאות לגבולות שצריך לברר בכל פרויקט, ולא טענות על חולשות שהתגלו ב־PDD Kit.

השאלה המקצועית אינה אפוא ״האם יש הוכחה?״ בלבד, אלא ״מה היקפה?״. עבור מנהלי פיתוח ואנשי אבטחה, מסמך ברור של ההנחות והחרגות הכיסוי עשוי להיות חשוב להבנת התוצאה לא פחות מהודעת הצלחה של כלי האימות.

04הזווית הישראלית: מכון ויצמן וצוותי הפיתוח בארץ

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

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

1. להגדיר תכונה אחת שרוצים לבדוק, במקום יעד כללי כמו ״מערכת בטוחה״.
2. להעביר את המפרט לביקורת משותפת של פיתוח, אבטחה ובעלי הדרישה העסקית.
3. לתעד אילו הנחות ורכיבים נמצאים בתוך גבולות ההוכחה ואילו נשארים בחוץ.
4. להמשיך בבדיקות רגילות, ולבחון מחדש את הכיסוי כשהקוד או הדרישות משתנים.

05מה צריך לבחון בהמשך

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

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