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