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