انتقاد للمقاييس المضللة في الأساليب الرسمية

تستخدم ورقة بحثية إحصائيات مضللة عند تطبيق الأساليب الرسمية للتحقق من صحة رمز نظام التشغيل. ينتقد الكاتب منهجية خاطئة تتمثل في مجرد مقارنة "نسبات البرهان إلى الكود"، لأنها تتجاهل اكتمال وتعقيد المواصفات. تشير المقالة إلى أن حجم البرهان له علاقة تربيعية تقريبية بحجم المواصفات، وأن تعقيد المواصفات أهم بكثير من حجم الكود. من خلال تحليل العديد من الأنظمة التي تم التحقق منها، يقدم الكاتب بيانات أكثر شمولاً، بما في ذلك حجم الكود، وحجم المواصفات، وحجم البرهان، ويبرز دور الوحدات النمطية في تقليل تكاليف التحقق، لكنه يلاحظ أيضًا أن الأنظمة المعقدة مثل seL4 يصعب تجميعها في وحدات نمطية. في النهاية، يناشد الكاتب مجتمع البحث التوقف عن استخدام مقياس "نسبة البرهان إلى الكود" عديم المعنى.