مهندسی نرم افزار با بهره گیری از دانش، نرم افزار های مقرون به صرفه ای را ارائه می نماید. در همین راستا درستی نرم افزارهای تولید شده مسئله مهمی است. به این منظور می توان از زبان صوری (فرمال)  بهره جست. در زمینه نرم افزار مبحثی بنام سیستم عاملگرا معرفی گردید.حال یکی از روش های عاملگرا به نام پرومتئوس  به وسیله تبدیلات گراف که یک روش صوری است ، معرفی می شود. البته  در این مقاله سعی شده از تمامی ویژگی های  ابزار صوری  برای رسیدن به یک سیستم فرمال به منظور کشف سریع خطا استفاده شود. بنابراین هدف اصلی تعریف پرومتئوس به زبان فرمال به صورت اتوماتیک در ابزار مربوطه به منظور ارزیابی روش خواهد بود.