أطلقت مايكروسوفت مفتوحة المصدر فرعاً من مكتبتها التشفيرية SymCrypt يحتوي على مواصفات رسمية وبراهين لتنفيذي Rust لـ ML-KEM وSHA-3. تُظهر هذه الإصدار منهجية حيث تُكتب خوارزميات الإنتاج بلغة Rust الآمنة وتُتحقق منها مقابل نماذج Lean المستمدة من المعايير باستخدام مجموعة أدوات Aeneas.
- تستخدم النهج أداة Aeneas لترجمة التمثيل متوسط المستوى لـ Rust إلى نماذج Lean نقية، مستغلةً قواعد ملكية Rust لتبسيط الاستدلال حول سلامة الذاكرة.
- صُممت المواصفات الرسمية لتعكس عن كثب المعايير العامة مثل NIST أو RFCs الخاصة بـ IETF، مما يتيح اختباراً قابلاً للتنفيذ مقابل المتجهات الرسمية ومراجعة بشرية سطراً بسطر.
- يتضمن الفرع مفتوح المصدر براهين كاملة لكود ML-KEM وSHA-3 المستخدم حالياً في إصدارات Windows Insider، مع خطط لتوسيع هذا سير العمل ليشمل AES-GCM وFrodoKEM وML-DSA.
توفر هذه المنهجية طبقتين من الضمان من خلال الجمع بين ضمانات سلامة الذاكرة في Rust وبراهين Lean للصحة الوظيفية، بهدف توسيع نطاق التحقق الرسمي لخوارزميات التشفير المستخدمة في الإنتاج.