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