لغة الاصطناعي المستخدمة لتمثل مطلبا برمجيات. متطلبات الرسمية الناتجة يمكن أن يثبت "الصحيح" من خلال طرق الإثبات لصحة. المعروف أيضا لغة متطلبات يمكن التحقق منها.