باختصار
التحقّق الصوري (Formal Verification) أن تثبت رياضيًا، وبتدقيق آلي، أن برنامجًا أو تصميمًا أو برهانًا يحقّق مواصفة محدّدة في كل الحالات الممكنة.
بالتفصيل
الاختبار العادي يجرّب أمثلة: أدخلنا هذا، فخرج ذاك. وهو مفيد، لكنه لا يخبرك بشيء عن الحالات التي لم تجرّبها. التحقّق الصوري يحاول أن يغلق هذه الفجوة: بدل «جرّبنا ألف حالة ونجحت»، يقول «أثبتنا أنها تنجح دائمًا».
من أشهر أدواته اليوم لغة Lean، التي يصفها موقعها بأنها لغة برمجة ومساعد براهين مفتوح المصدر لكتابة كود صحيح ومتحقَّق منه صوريًا، بنواة موثوقة صغيرة. وتذكر الصفحة استخدامات صناعية: Microsoft Research تتحقّق عبرها من خوارزميات تشفير تعمل في الإنتاج داخل مكتبة SymCrypt، وAWS تتحقّق بها من مكوّنات لغة الصلاحيات Cedar.
وفي الذكاء الاصطناعي صار التحقّق الصوري شريكًا للنماذج: النموذج يكتب البرهان، وLean يدقّق كل خطوة. هكذا كُتب برهان OpenAI لمسألة نافييه-ستوكس. لكن للطريقة حدًّا يذكّر به المتابعون: Lean يدقّق كل خطوة منطقية، لكنه لا يجعل البرهان مفهومًا للبشر. وتذكّر أن الإثبات يكون على المواصفة التي كتبتها أنت، فإذا كانت المواصفة خاطئة، أثبتَّ الشيء الخطأ بإتقان.
مثال عملي
إذا قست زوايا عشرة مثلّثات ووجدت مجموعها 180 درجة في كل مرّة، فهذا اختبار. أمّا إذا أثبتّ ذلك بالهندسة لكل مثلّث مستوٍ ممكن، فهذا برهان.
والتحقّق الصوري هو أن تطلب من الحاسوب أن يراجع هذا البرهان خطوة خطوة، دون أن يقبل منك «من الواضح أن».
مصطلحات مرتبطة
- Proof Assistant — مساعد البراهين.
- Automated Theorem Proving — الإثبات الآلي للمبرهنات.
- Mutation Testing — اختبار الطفرات البرمجية.
- Specification — المواصفة.
المصادر: Lean، Scientific American، The Decoder — 2026-10-13, 2026-10-17
