قال المحقق الشكلي: «مثبَتة». والرقاقة ما زالت معطوبة.
في المرة الأولى التي كذبت فيها إحدى أدواتنا عليّ، فعلت ذلك بأدب. أعاد المحرك الشكلي علامة صح خضراء. كل خاصية طلبنا منه إثباتها عادت مثبَتة. بدت مكتبة التوكيدات مكتملة. على الورق، كان التصميم قد جرى التحقق منه.
استغرقنا يومين لندرك أن الشهادة كانت بلا قيمة — وأن كل ما افترضته حول التحقق بالذكاء الاصطناعي في أشباه الموصلات كان يحمينا من العطل الخطأ.
كانت الخصائص قد وُلِّدت بواسطة نموذج لغوي كبير لفّفناه حول المحرك الشكلي — تمامًا من نوع العروض التوضيحية البراقة لتصميم الرقائق بالذكاء الاصطناعي الوكيلي التي كان الجميع يبنيها. وكان المحرك قد أثبتها في أجزاء من الألف من الثانية، وهو ما كان ينبغي أن يكون العلامة المُنبِّهة. لقد أُثبتت لأن الشروط التي كانت ستختبرها لم تتحقق قط. خاصية تقول "كل طلب يحصل في النهاية على منح" تكون صحيحة على نحو تافه إذا كان الطلب لا يمكن أن يحدث أبدًا. لم يكن المُحلِّل مخطئًا. لقد أجاب عن السؤال الذي طرحناه من غير قصد، وكان السؤال فارغًا. تلك هي اللحظة التي فهمت فيها ما يتعين على خطوط أنابيب التحقق بالذكاء الاصطناعي هذه أن تدافع عنه فعليًا — ولماذا لم يكن أحد تقريبًا ممن يبيعونها يدافع عن الشيء الصحيح.
أريد أن أخبرك بما وجدناه، لأن فئات العلل التي تقتل الرقائق الحديثة ليست تلك التي تعلن الصناعة عن قدرتها على اكتشافها. نبني خطوط أنابيب تحقق مخصصة لفرق الرقائق بلا مصانع — نماذج مفتوحة الأوزان مضبوطة بدقة وملفوفة حول المحرك الشكلي الذي يملكه الفريق بالفعل، وتعمل بالكامل على أجهزتهم الخاصة — وقد نشأ النهج بأكمله من الوقوع في هذا الخطأ أولًا. يمكنك رؤية شكله على veriprajna.com/solutions/semiconductor-ai-verification. لكن النهج لا يصبح منطقيًا إلا بعد أن تشاهد تصميمًا "ناجحًا" يفشل.
رقم ينبغي أن يُرعب كل مدير مالي لشركة بلا مصانع
إحصائية واحدة تؤطر المشكلة بأكملها. دراسة التحقق الوظيفي لعام 2024 من Wilson Research Group / Siemens EDA — أطول معيار مرجعي مستمر في الصناعة — وضعت نجاح السيليكون الأول عند 14%. أدنى مستوى وصل إليه خلال عشرين عامًا من التتبع. في عام 2020 كان هذا الرقم حوالي 32%. لقد انخفض إلى أقل من النصف في أربع سنوات.
ليست هذه قصة عن مهندسين أصابهم الكسل. إنها قصة عن تعقيد يتجاوز الأدوات، وعن مواصفة تتحور أسرع من منصة الاختبار التي تلاحقها. وجدت الدراسة نفسها أن ما يقارب 70% من إعادات التصنيع تنتج عن أخطاء مرتبطة بتغييرات المواصفات — وليست علل منطق بحتة.
لم ينخفض نجاح السيليكون الأول لأن فرق الرقائق ساءت. انخفض لأن المواصفة تتحرك الآن أسرع مما يستطيع التحقق أن يغلقها.
جلست مع رقم 70% هذا وقتًا طويلًا، لأنه يدين بهدوء الكثير من عروض "الذكاء الاصطناعي لتصميم الرقائق". إذا كانت معظم إعادات التصنيع تأتي من انحراف المواصفات، فإن أداة لا تكتشف سوى علل المنطق تعالج شريحة من المشكلة وتسميها الفطيرة بأكملها.
وتكلفة الخطأ وحشية على نحو يستهين به أهل البرمجيات. مجموعة أقنعة بحجم 5 نانومتر تكلف 10–20 مليون دولار. عند 3 نانومتر تقترب من 40 مليون دولار، مع أكثر من سبعين طبقة قناع تتضمن أكثر من عشرين طبقة EUV. تكلف عملية إخراج التصميم الكاملة بحجم 2 نانومتر الآن ما يقارب 725 مليون دولار شاملةً كل شيء. وعندما يفلت شيء ما، تعني إعادة التصنيع انزلاقًا في الجدول الزمني من 3 إلى 6 أشهر فوق فاتورة الأقنعة. في نافذة منتج مدتها ثمانية عشر شهرًا، يمكن لانزلاق مدته ستة أشهر أن يمحو نصف إيرادات الرقاقة طوال عمرها. لا يرى المدير المالي التحقق مركزَ تكلفة. يراه تأمينًا ضد خطأ واحد من ثمانية أرقام.
كيف يهلوس نموذج لغوي كبير فعليًا داخل العتاد؟
فريقك يستخدم بالفعل النماذج اللغوية الكبيرة مع Verilog. لن أتظاهر بغير ذلك، ولا ينبغي لأي شخص يبيع لك أن يتظاهر. مجال البحث حقيقي الآن — انتقلت الأوراق البحثية حول كتابة النماذج اللغوية الكبيرة لـ Verilog من ورقة واحدة في عام 2020 إلى أربعٍ وستين في عام 2025. في المسائل الأصعب ضمن معيار VerilogEval، تحقق النماذج من فئة GPT-4 حوالي 43% من الصحة الوظيفية. مفيدة. غير جديرة بالثقة.
السؤال المثير للاهتمام ليس ما إذا كانت النماذج تساعد. بل كيف تفشل، لأن أنماط الفشل لا تشبه حالات الفشل التي دُرِّب مهندسو البرمجيات على الخوف منها. بعد ليالٍ متأخرة كافية من التحديق في سبب فساد شيفرة RTL "التي تبدو صحيحة"، بدأت أُصنِّف حالات الفشل إلى خمس فئات.
الأولى هي غير المؤذية. الهلوسة النحوية — شيفرة لا تُترجَم ببساطة. يكتشفها Verilator أو الواجهة الأمامية للتخليق في ثوانٍ. الجميع يعرف بالفعل كيفية التعامل مع هذا، وهي الفئة التي يشير إليها الناس عندما يريدون الادعاء بأن المشكلة قد حُلَّت.
الثانية هي حيث يبدأ الألم. الهلوسة الدلالية، والحالة النموذجية هي الإسناد الحاجب مقابل غير الحاجب. نموذج مُدرَّب على Python وC يقرأ Verilog كما لو أن العبارات تُنفَّذ من الأعلى إلى الأسفل. لذا يكتب إسنادًا حاجبًا — علامة = بسيطة — داخل always_ff كتلة مُوقَّتة حيث تتطلب اللغة الإشارة غير الحاجبة <=. أراد المصمم خط أنابيب من دورتين. مع الإسنادات الحاجبة، تقرأ المرحلة الثانية القيمة الجديدة للأولى، لا القديمة، وتُشحَن الرقاقة بتجاوز من دورة واحدة بدلًا من ذلك. بعض أدوات المحاكاة تجدول الأحداث بترتيب يُخفي التسابق كليًا. تُحاكى على ما يرام. وتُخلَّق إلى الآلة الخطأ.
الفئة الثالثة هي التي علّمتني أن أُبقي مواصفة AMBA مفتوحة على شاشة ثانية. الهلوسة البروتوكولية. الشيفرة تُترجَم، وتجتاز تسعين بالمئة من الاختبارات الموجَّهة، ثم تؤكّد إشارة صحة بيانات الكتابة قبل أن يكون التابع جاهزًا لقبول العنوان — انتهاك لمصافحة AXI. أو تُبقي إشارة صحة مرتفعة بينما تُقلِّب البيانات تحتها. أو تُخِلّ ببند فرعي مدفون في الصفحة 84 من مواصفة الناقل لم يحفظه أي إنسان. تعمل الرقاقة على نحو مثالي على منصة اختبارك الداخلية، وتتجمّد في اللحظة التي تُوصَل فيها بمتحكم ذاكرة من طرف ثالث. لا يمكنك التغلب على هذا بالقوة عبر مزيد من دورات المحاكاة. تكتشفه بمكتبات توكيدات مُتحقَّق منها مسبقًا ومكتوبة مقابل كل بروتوكول.
الفئة الرابعة هي التي خدعتنا، وهي الخطيرة.
لماذا تُعَدّ كلمة "مثبَتة" أخطر كلمة في تقرير تحقق؟
الهلوسة الفراغية. يُولِّد النموذج توكيدًا بلغة SystemVerilog. يُثبته المحرك الشكلي. فتشحن. وكانت الخاصية صحيحة على نحو تافه لأن مُقدَّمها — جزء "الشرط" — لم يصبح صحيحًا في المقام الأول.
تخيّل خاصية مُحكِّم: إذا أُثير طلب، فيجب أن يتبعه منح خلال عدد ما من الدورات. الآن افترض أن النموذج نفسه، محاولًا أن يكون مفيدًا، كتب أيضًا افتراضًا يُجبر إشارة الطلب على أن تكون منخفضة. يُثبت المحرك الشكلي بإخلاص خاصية المنح في أجزاء من الألف من الثانية، لأنه لا يوجد طلب لينتهكها أبدًا. قد يكون المُحكِّم الحقيقي تحتها مُعطَّلًا تمامًا. تقول الشهادة "مثبَتة". وهي بلا قيمة.
الإثبات الشكلي الذي يُنفَّذ في أجزاء من الألف من الثانية ليس سريعًا. إنه مريب. قد يكون المحرك لم يُثبت شيئًا على الإطلاق.
هذه ليست مخاطرة هامشية. تنشر Siemens تحذيرات بشأن الإثباتات الفارغة منذ عام 2017، وما زال المجال يشحن تدفقات دون فحص تلقائي للفراغ. عندما أخبر الناس أن تدفق تحقق شكلي دون كشف الفراغ أسوأ من عدم وجود تحقق شكلي على الإطلاق، يظنون أنني أُبالغ. لست كذلك. عدم وجود تحقق يتركك خائفًا على النحو المناسب. أما كلمة "مثبَتة" الفارغة فتتركك واثقًا ومخطئًا، مع كتلة مُوقَّعة متجهة إلى إخراج التصميم. تلك هي الإخفاقة التي كادت تُشحَن في نموذجنا الأولي المبكر، وقد غيّرت إلى الأبد ما نبنيه.
الفئة الخامسة هي التي لا تستطيع المحاكاة رؤيتها بنيويًا. النقاط العمياء لعبور نطاقات الساعة. يقرأ النموذج اللغوي الكبير أسماء الإشارات؛ لكنه لا يُدرك نطاقات الساعة. لذا يوصل إشارة من نطاق وحدة معالجة مركزية بتردد 2 جيجاهرتز مباشرةً إلى قلّاب نطاق طرفي بتردد 400 ميجاهرتز، متخطيًا مُزامِن القلّاب المزدوج الذي يمنع اللااستقرار. لا تُنمذِج محاكاة RTL اللااستقرار — لذا يجتاز الاختبار الانحداري، في كل مرة، ويتجمّد السيليكون في الميدان. لهذا تلتهم علل عبور نطاقات الساعة مجموعات الأقنعة. ولهذا أيضًا فتحت Accellera معيار تشغيل بيني لـ CDC/RDC في عام 2024: كان التشرذم عبر أدوات CDC التجارية قد بلغ سوءًا يكفي لكسر الإقرار النهائي.
تشترك الفئات من الثانية إلى الخامسة في خاصية مرعبة واحدة: إنها تجتاز المحاكاة. إنها لا تظهر إلا في السيليكون. تلك هي المجموعة الفرعية من العلل التي ما زالت تُفجّر عمليات إخراج التصميم، وهي بالضبط المجموعة الفرعية التي يتركها عرض "يكتشف علل المنطق" على الطاولة.
جدار المورّدين الذي يقف فريق الرقائق أمامه فعليًا
عندما ذهبت أبحث عن مساعدة مستقلة حقًا في عملية إخراج تصميم، وجدت خيارات أقل مما كان لديّ قبل بضع سنوات — وليس هذا حنينًا، بل هو بنية السوق. مورّدو EDA الثلاثة الذين يستطيع قائد تحقق التصميم أن يختار منهم فعليًا — Synopsys وCadence وSiemens — انتقلوا من أقل من 75% من السوق قبل عقد إلى أكثر من 85% اليوم. أضِف استحواذَ Synopsys على Ansys بقيمة 35 مليار دولار ويسيطر الأربعة الكبار على نحو 90%. لقد ضاق الميدان الذي تتسوق فيه شركة ناشئة بلا مصانع، ولم يتسع، تمامًا في الوقت الذي ازدادت فيه المشكلة صعوبة.
والشركات الراسخة لا تقف مكتوفة الأيدي بشأن الذكاء الاصطناعي. أطلقت Synopsys AgentEngineer في مارس 2026، وهو تدفق عمل تحقق وكيلي يزعم إنتاجية أعلى بمرتين إلى خمس مرات، ويستقر فوق VC Formal — أكثر مكدّس وكيلي من مورّد جديرٍ بالثقة قيّمته. أعلنت Cadence عن ChipStack AI Super Agent في فبراير 2026 وتُشغّل Cerebrus AI Studio لتنفيذ مدفوع بالتعلّم المعزَّز، مع بقاء JasperGold المحرك الشكلي المعياري الذهبي الذي يُقاس عليه كل الآخرين. أقول ذلك دون تحفّظ: JasperGold وVC Formal ممتازان حقًا. وأي شخص يفتتح عرضه بالحطّ منهما فقد أخبرك أنه لم يُغلق قط عملية إخراج تصميم حقيقية.
المشكلة في التسعير والموقف. جرى خط JasperGold الأساسي التاريخي عند حوالي 225 ألف دولار زائد 45 ألف دولار لكل مقعد — جيد لشركة بلا مصانع كبيرة، بعيد المنال عن الشركات الناشئة في مراحلها المبكرة العاملة على RISC-V ومُسرِّعات الذكاء الاصطناعي التي تقوم بأكثر الأعمال إثارةً للاهتمام. وأحدث ميزات الذكاء الاصطناعي لدى الشركات الراسخة سحابية أولًا، وهو ما يصطدم رأسًا بالمتطلب الوحيد الذي لن يتنازل عنه هؤلاء العملاء. المزيد عن ذلك بعد لحظة.
ثم هناك موجة الشركات الناشئة، وهي صاخبة. في آخر مؤتمري DAC وDVCon، كان قائد تحقق تصميم أعمل معه قد تلقّى عروضًا من ثماني شركات مختلفة لـ "الذكاء الاصطناعي الوكيلي لتصميم الرقائق" في ربع سنة واحد. ChipAgents جمعت 74 مليون دولار حتى أوائل 2026 وتزعم إنتاجية تصميم وتحقق أعلى بعشر مرات. Normal Computing جمعت 50 مليون دولار بقيادة Catalyst Fund التابع لـ Samsung، وتبني الشَّكْلنة التلقائية — نماذج لغوية كبيرة تترجم نية المهندس مباشرةً إلى خصائص شكلية وتُثبتها — وتقول إن نصف أكبر عشر شركات لتصميم أشباه الموصلات في العالم تستخدمها. وهناك المزيد: MooresLabAI التي تُولِّد منصات اختبار كاملة، وBronco في تحليل الانحدار، وSilimate في التنبؤ بالقدرة والأداء والمساحة.
بعض هذه حقيقي. لا أحد منها يحل مشكلة العميل الفعلية، وهي أنه اشترى الآن ثلاثًا من هذه الأدوات النقطية ولا فكرة لديه عن كيفية جعلها تعمل معًا داخل تدفق الإقرار النهائي الذي يثق به بالفعل.
قصة توظيف التعلّم المعزَّز في التنسيب التي لا أحد يريد قولها بصوت عالٍ
هناك إغراء موازٍ في تصميم الرقائق يتجاوز التحقق: استخدام التعلّم المعزَّز للقيام بالتخطيط الأرضي الفيزيائي — تقرير أين تجلس الكتل الكبيرة على الرقاقة. إنه مغرٍ، والنتيجة الأكثر استشهادًا بها متنازَع عليها بطريقة تتخطّاها معظم العروض بملاءمة.
زعمت ورقة Google في مجلة Nature لعام 2020 أن التعلّم المعزَّز يتفوق على التلدين المُحاكى في تنسيب الماكرو، وقد استُخدم في سيليكون حقيقي — شُحنت أجيال TPU به. لكن في عام 2023، أضافت Nature ملاحظة تحريرية بعد إثارة مخاوف منهجية. نشر Igor Markov، الموجود الآن في Synopsys، نقدًا سطرًا بسطر مقارنته الرئيسية يصعب نسيانها: استغرق نهج التعلّم المعزَّز 32.31 ساعة، واستغرق خط أساس تلدين مُحاكى مُضبوط 12.5 ساعة، وأنهت أداة Cadence تجارية المهمة نفسها في 0.05 ساعة. ردّت DeepMind بورقة بعنوان "That Chip Has Sailed". وبعد سنوات، لم يؤكّد أي تكرار خارجي مستقل الادعاءات الأصلية، ولا يزال كلّ من النقد والردّ قائمَين.
أطرح هذا بسبب ما يحدث عندما يعرض مستشار تنسيب التعلّم المعزَّز على فريق شكلي حقيقي ويتظاهر بأن الجدل غير موجود. يشمّونه خلال عشر دقائق، وتكون قد خسرت القاعة. الموقف الصادق هو أن هناك زوايا حقيقية — التخطيط الأرضي الواعي حراريًا للشرائح الصغيرة والدوائر المتكاملة ثلاثية الأبعاد، والتخطيط التناظري، وتحسين ملكية RISC-V الفكرية على أدوات مفتوحة — حيث يستحق النهج الهجين مكانه. أما الهجوم الأمامي على محركات تنسيب الشركات الراسخة فلا يستحق. معرفة الفرق، وقوله بصوت عالٍ، هي العمل كلّه.
ما الذي تغيّر بعد أن خدعتنا أداتنا
إذًا، ها هو المكان الذي قادتنا إليه كارثة الإثبات الفارغ. توقفنا عن محاولة بناء ذكاء اصطناعي أفضل يكتب Verilog، لأن ذلك سباق مزدحم بثمانية متسابقين ممولين، وبدأنا نبني الشيء الذي لا يبيعه أيٌّ منهم: طبقة التكامل المحايدة تجاه المورّدين التي تجعل أدوات الفريق الحالية جديرة بالثقة.
بشكل ملموس، يعني ذلك بضعة قرارات، فرض كلًّا منها إخفاقٌ رأيناه. نضبط بدقة نموذجًا مفتوح الأوزان — Qwen Coder أو Llama أو أيًّا كان المناسب — على مجموعة العميل الخاصة من شيفرة RTL، ومواصفاتهم، وسجل عللهم السابق، لأن نموذجًا لم يرَ أسلوب بيتك يهلوس مقابله. نلفّه حول أي محرك شكلي يملكه الفريق بالفعل: JasperGold أو VC Formal أو Questa Formal أو SymbiYosys مفتوح المصدر. لا نطلب منهم أبدًا اقتلاع الأداة المعيارية الذهبية التي يثقون بها بالفعل. وكل خاصية يقترحها النموذج تمر عبر فحوصات الفراغ والتغطية قبل أن يُسمح لأي أحد بقراءة كلمة "مثبَتة" — لأننا تعلّمنا بالطريقة المكلفة أن الإثبات غير المحروس مسرحية.
مكتبات التوكيدات المُتحقَّق منها مسبقًا لا تقل أهميةً عن النموذج. بالنسبة إلى نواة RISC-V، تُشحَن المنصة الشكلية مع فحوصات امتثال AXI4 وAHB وTileLink، وتوكيدات مخاطر خط الأنابيب، ولوحة نتائج التحميل والتخزين، وخصائص صحة وحدة التنقيح — الأشياء التي تكتشف الهلوسة البروتوكولية والدلالية قبل أن يكتشفها السيليكون. هذا ليس تخمينيًا. وجدت شركة الاستشارات الشكلية Axiomise أكثر من 65 علة في Ibex، نواة RISC-V المفتوحة داخل OpenTitan من Google، بما في ذلك علل تعليمات التفرّع في وحدة التنقيح التي لم يكن بمقدور سوى التحقق الشكلي اكتشافها. التحقق الشكلي يعمل على RISC-V. الشيء النادر ليس المنهج؛ بل هو فريق يعرف كيف يستخدمه.
الفرصة الحقيقية هنا لم تكن قط نموذج Verilog أذكى. بل كانت منصةً صادقةً ملفوفة حول الأدوات المكلفة التي يثق بها الفريق بالفعل.
لماذا لن تُشغّله ببساطة في السحابة؟
يسألني الناس هذا باستمرار، والجواب هو السبب نفسه الذي يجعل كل شركة ناشئة سحابية أولًا في مجال الذكاء الاصطناعي لـ EDA ميتةً عند الوصول لدى العملاء الذين أهتم بهم: شيفرة RTL هي جواهر التاج، وهي لا تغادر المبنى.
شيفرة نقل مستوى السجلات لشركة بلا مصانع هي الشركة. يحتاجها عملاء الدفاع والفضاء معزولةً عن الشبكة، أحيانًا في منشأة آمنة. تريدها الفرق التجارية بلا مصانع محليةً، سحابةً خاصةً افتراضيةً كحدٍّ أدنى مطلق. لذا نُشغّل كل شيء على أجهزة العميل الخاصة — استدلال vLLM أو ما شابه على عنقود H100 أو H200 الموجود لديهم، واسترجاع محلي على مجموعتهم الخاصة، دون أن تعبر شيفرة RTL حدود الشبكة، أبدًا. أحدث ميزات الشركات الراسخة الوكيلية سحابية أولًا؛ وهذه ميزة لهم وعائق كامل لفريق رقائق حسّاس تجاه الملكية الفكرية. أكبر فرصة أراها ليست مشكلة خوارزميات على الإطلاق. إنها مشكلة نشر وتكامل قرر الناس أصحاب أفضل الخوارزميات ألّا يحلّوها.
السؤال الآخر يأتي من فرق السيارات، وهو الذي يقرر كل شيء بالنسبة إليهم. اشحن رقاقةً في سيارة عند مستوى ASIL C أو D — مستويات سلامة النزاهة حيث يتوقف ISO 26262 عن مجرد اقتراح التحقق الشكلي ويبدأ في فرضه — وعندئذٍ يتعين على الأداة نفسها أن تحمل حزمة تأهيل TCL2 أو TCL3. محركات الشركات الراسخة الأساسية لديها ذلك الاعتماد من طرف ثالث؛ أما أداة ذكاء اصطناعي جديدة كليًا فلا. لقد شاهدت أداةً أفضل حقًا تُوضَع على الدكة في برنامج سيارات لهذا السبب بالضبط: لا حزمة تأهيل، لا مكان في تدفق الإقرار النهائي، نهاية المحادثة. لذا لا نحاول أن نكون الأداة المؤهَّلة. نساعد الفرق على تشغيل مساعدة الذكاء الاصطناعي جنبًا إلى جنب مع محركات الشركات الراسخة المؤهَّلة دون كسر سلسلة التأهيل — لأنه في مجال السيارات، الأداة المتفوقة تقنيًا التي لا تستطيع النجاة من تدقيق لا تساوي شيئًا.
الشهادة ليست الرقاقة
أظل أعود إلى ذينك اليومين اللذين قضيناهما نثق في علامة صح خضراء لا تعني شيئًا. لم يكن الدرس "النماذج اللغوية الكبيرة سيئة في Verilog". إنها تتحسن كل ربع سنة. كان الدرس أنه في العتاد، الفجوة بين يبدو مُتحقَّقًا منه ومُتحقَّق منه فعلًا تُقاس بمجموعات أقنعة من ثمانية أرقام وانزلاقات مدتها ستة أشهر — والأدوات المندفعة إلى هذا المجال تتسابق في معظمها لجعل جزء "يبدو مُتحقَّقًا منه" أسرع.
على مجموعة أقنعة بقيمة 10 ملايين دولار، "مثبَتة" لا يمكنك تتبّعها إلى إثبات غير فارغ، منفّذة على أجهزة تتحكم بها، مقابل توكيدات كتبها شخص قرأ الصفحة 84 من المواصفة — هذه ليست تحققًا. إنها أمل بقيم إنتاجية جيدة. إذا أردت أن ترى كيف نُميّز الفرق، فهو مبسوط بالكامل على veriprajna.com/solutions/semiconductor-ai-verification.
لا تكترث الرقاقة بما يقوله التقرير. إنها تفعل فقط ما بُني السيليكون فعليًا ليفعله. التحقق هو انضباط جعل هذين الأمرين متطابقين — واللحظة التي يخبرك فيها ذكاء اصطناعي بأنهما متطابقان في أجزاء من الألف من الثانية، هي بالضبط اللحظة التي ينبغي أن تمدّ فيها يدك إلى المواصفة.
