मैं किसी स्पेक के विरुद्ध कोड तो सत्यापित कर सकता हूं, लेकिन स्पेक को स्वयं क्यों नहीं?

स्मार्ट कॉन्ट्रैक्ट के लिए फॉर्मल वेरिफिकेशन यह साबित करता है कि कोड एक लिखित विनिर्देश को संतुष्ट करता है, लेकिन यह तय नहीं कर सकता कि वह विनिर्देश वास्तव में कॉन्ट्रैक्ट के इच्छित व्यवहार को दर्शाता है या नहीं। अत्याधुनिक स्वचालित ऑडिट टूल को कवर करने वाले 2025 के MDPI सर्वेक्षण में पाया गया कि वे प्रोडक्शन में मिले शोषण योग्य बग्स का केवल 8 से 20 प्रतिशत ही पकड़ पाते हैं, जबकि निम्न-स्तरीय सिंटैक्स पैटर्न की 90 प्रतिशत से अधिक कवरेज रिपोर्ट करते हैं। असली खामी स्पेक में है: तार्किक त्रुटियां, एसेट लॉक कंडीशन और ओरेकल अनुमान लगभग कभी भी स्पेक में नहीं आते क्योंकि इंजीनियर किसी exploit के ज़रूरत को उजागर करने से पहले उन्हें सूचीबद्ध करना नहीं जानते। NDSS 2025 PropertyGPT पेपर सीधे कहता है कि समुदाय में अभी भी प्रभावी फॉर्मल वेरिफिकेशन के लिए व्यापक गुणों की स्वचालित उत्पत्ति का अभाव है। हर वह ऑडिट जो एक अधूरे स्पेक के विरुद्ध कॉन्ट्रैक्ट को क्लीयर करता है, एक सुरक्षित प्रणाली के बजाय एक झूठे आत्मविश्वास की निचली सीमा तैयार करता है।