يُمكّن التحقق الأساسي المبرمجين من بناء برامج تم إثبات تأكيدها بشكل تجريبي بمستويات عالية من الثقة في مجموعة واسعة من المجالات المهمة. ومع ذلك، يظل تكلفة إنتاج برمجيات مُحققة أساسياً مرتفعة بشكل يُشكل عائقاً أمام معظم المشاريع، نظراً لاحتياجها إلى جهد يدوي كبير من خبراء مدربين تدريباً عالياً. في هذا البحث، نقدّم "بروفربوت9001"، وهو نظام بحث عن البراهين يستخدم تقنيات التعلم الآلي لإنتاج براهين صحة البرمجيات في أدوات البرهان التلقائي التفاعلي. ونُظهر كفاءة بروفربوت9001 على مهام البرهان المستمدة من مشروع برهان عملي كبير، وهو مترجم C المُحقق CompCert، ونُثبت أنه قادر على أتمتة البراهين التي كانت تُجرى يدوياً سابقاً، حيث يُنتج تلقائياً براهين لـ 27.5٪ من عبارات النظريات في مجموعة اختبارنا، عند دمجه مع أدوات قائمة على المحّلّات (solvers). وبلا أي محّلّات إضافية، نُظهر معدل إنجاز برهان يُعدّ أفضل بـ 4 أضعاف مقارنة بأفضل النماذج السابقة القائمة على التعلم الآلي لإنتاج البراهين في نظام Coq.