يبني الطفل لعبة بسيطة في سكراتش: تظهر الشخصية في المنتصف وتقفز فوراً إلى الزاوية. الحركة الأولى تختفي بين الإطارات ولا يراها أحد. إزالة هذا الأمر آمنة. لكن كيف يعرف المُحسِّن التلقائي ذلك؟ اليوم، يحتوي مستودع سكراتش على عشرات الملايين من المشاريع التي كتبها مؤلفون صغار. خطأ من المُحسِّن قد يُشوِّه مقصدهم دون أن يُلاحَظ.

الحل يشبه التفتيش الجمركي. يمسح المُحسِّن غير الموثوق المشروع، ويبني غرافاً للاعتماديات ويقترح حذف زي غير مستخدم أو أمر ميت مثلاً. يُرفق بالتعديل «شهادة» — تصريح رقمي يحدد نوع التغيير وشروط السلامة. المفتش المراقب الموثوق، الذي لا يصدق كلمة واحدة، يعيد تحليل نسختي البرنامج من جديد. يعيد حساب جميع الشروط. تعمل عدسة الملاحظة (مجموعة الأحداث المرئية للاعب) كدليل رئيسي: إذا تمت كتابة مورد فوقه قبل أن يصبح قابلاً للملاحظة، يمكن حذفه. هذه هي المبرهنة المركزية حول الإطار التعاوني (cooperative frame)، المُبرهَنة في لين. لن تخفي الشهادة أي حيلة.

أظهرت التجربة على 300 مشروع حقيقي: حصل 283 مشروعاً على تحسين آمن واحد على الأقل، أي بنسبة 94.3%. تم بشكل أساسي تنظيف الموارد غير المستخدمة، ولكن في 17 حالة تمت أيضاً إزالة كتابات ميتة لغوياً (semantically dead writes). الأهم من ذلك، أن هجوماً خصومياً مكوّناً من 4278 تعديلاً حُبكت فيها أخطاء عمداً لم يخترق ولو مرة واحدة. رفض المُراقب جميع الخيارات الخطرة. ولم يسجّل الوحي التفاضلي (differential oracle)، الذي قارن سلوك البرنامجين الأصلي والمُحسَّن على آلة افتراضية، أي اختلاف.

لأول مرة، يتم بناء نظام للغة موازية موجّهة بالأحداث (event-driven)، حيث يحمل كل تغيير شهادة قابلة للتحقق. وهذا ينقل انضباط المصرّفات المُحقَّقة (verified compilers) إلى عالم تكون فيه كلفة الخطأ عالية بشكل خاص. مبرهنة الإطار التعاوني مُوسوَطة بنوع المورد وعدسة الملاحظة — برهان واحد يغطي فصيلة كاملة من التحسينات. وهي تؤمّن اكتمالاً معلوماتياً لشروط الصحة، فتقصي أي قنوات مراقبة غير متوقعة. الأساس الموثوق مضغوط: 9 921 سطراً بلغة بايثون (Python) و5 909 أسطر من البراهين في لين — حجم يمكن تدقيقه من قبل فريق صغير. مع ذلك، لا يحتاج هذا الأسلوب إلى افتراضات احتمالية أو استدلال بايزي: فهو يمنح ضمانات مطلقة. يمكن النظر إلى البرنامج باعتباره نظاماً ديناميكياً، وتحقّقه كتحليل حتمي، وليس عملية عشوائية.

جمرك الكود يعمل الآن. في المستقبل، سيتمكن من فحص التعديلات التي يقترحها الذكاء الاصطناعي، وسيشكل أساساً لمساعدي ذكاء اصطناعي موثوقين. أما الآن، فالمفتش جاهز للعمل: حين يضغط الطفل على «ابدأ»، سيبقى قصده سليماً.