Loading...
श्रृंखला: Formal Verification Series · 3 का भाग 1 पाठक-वर्ग: बिल्कुल नए लोग। गणित, प्रोग्रामिंग या क्रिप्टोग्राफी की किसी पृष्ठभूमि की अपेक्षा नहीं है। आप क्या समझकर जाएंगे: सॉफ़्टवेयर के सही होने को सिद्ध करने का अर्थ, यह परीक्षण से मूलभूत रूप से अलग क्यों है, machine-checked proof क्या होता है, और ऐसा प्रमाण वास्तव में क्या वादा कर सकता है उसकी सटीक (और ईमानदार) सीमाएँ।
अधिकांश सॉफ़्टवेयर पर भरोसा इसलिए किया जाता है क्योंकि उसका परीक्षण किया गया है: हम उसे कई इनपुट पर चलाते हैं और उसका व्यवहार देखते हैं। औपचारिक सत्यापन एक अधिक साहसी प्रश्न पूछता है। क्या हम गणितीय निश्चितता के साथ सिद्ध कर सकते हैं कि कोई सिस्टम हर संभव इनपुट के लिए वही करता है जो उसे करना चाहिए, उनमें भी जिन्हें आज़माने का किसी ने कभी सोचा तक नहीं? यह लेख उस विचार को मूल से निर्मित करता है। पहले अंतर्ज्ञान, प्रतीक तभी जब उनकी आवश्यकता हो।
यह एक सच्ची कहानी है, और यही इस श्रृंखला के होने का कारण है।
2022 में, गोपनीयता-केंद्रित क्रिप्टोकरेंसी Zcash ने Orchard नामक एक नया shielded pool लॉन्च किया, जिससे लोग राशि छिपाकर लेन-देन कर सकते थे। चार वर्षों तक उसने बिना किसी त्रुटि के काम किया और बार-बार पेशेवर ऑडिट पास किए। फिर, मई 2026 में, एक सुरक्षा शोधकर्ता ने अंतर्निहित गणित पर सावधानी से तर्क करते हुए (AI टूलिंग की मदद से) सिस्टम के गणित में एक under-constrained स्थान खोजा। वह एक कमी हमलावर को असीमित मात्रा में नकली धन बनाने दे सकती थी, और चूँकि राशियाँ छिपी हुई थीं, किसी को यह होता हुआ दिखता भी नहीं। यह दोष पूरे समय मौजूद था।
इसे परीक्षण ने नहीं पकड़ा। चार वर्षों तक हर परीक्षण पास हुआ था। इसे किसी ऐसे व्यक्ति ने पकड़ा जिसने गणित पर तर्क किया। और जब टीम ने इसे ठीक किया, तो उन्होंने केवल पैच लगाकर आगे नहीं बढ़ गए। उन्होंने 2,700 से अधिक अलग-अलग प्रमेयों पर आधारित एक machine-checked mathematical proof लिखा कि प्रतिस्थापन में इस प्रकार का दोष बिल्कुल नहीं हो सकता।
यही औपचारिक सत्यापन है, और इससे आपको यह मिलता है: “हमने बहुत-से मामले आज़माए और वे काम कर गए” नहीं, बल्कि “हमने सिद्ध किया कि यह हर मामले में सही है।” उन सिस्टमों के लिए जहाँ छूटा हुआ एक मामला विनाशकारी हो सकता है (धन, विमान, चिकित्सा उपकरण, क्रिप्टोग्राफी), यह अंतर ही सब कुछ है।
परीक्षण के blind spot का नाम दशकों पहले कंप्यूटर वैज्ञानिक Edsger Dijkstra ने दिया था, और वह आज भी सत्य है:
परीक्षण बगों की उपस्थिति दिखा सकता है, पर उनकी अनुपस्थिति कभी नहीं।
यदि कोई परीक्षण पास होता है, तो आप इतना सीखते हैं कि सिस्टम उस इनपुट पर काम करता है। जिन इनपुट को आपने नहीं आज़माया उनके बारे में आप कुछ नहीं सीखते, और खतरनाक बग लगभग हमेशा उन्हीं मामलों में होते हैं जिन्हें किसी ने नहीं आज़माया।
कल्पना कीजिए कि आप हज़ार दरवाज़ों वाली इमारत के ज़िम्मेदार हैं, और आपका काम यह सुनिश्चित करना है कि रात में हर दरवाज़ा बंद हो।
अंतर वास्तविकता का नमूना लेने और डिज़ाइन के किसी गुण को सिद्ध करने के बीच है। परीक्षण नमूने लेता है। औपचारिक सत्यापन सिद्ध करता है। यही पूरा विचार है, और बाकी सब इसे कठोरता से करने की व्यवस्था है।
हर औपचारिक सत्यापन, चाहे कितना भी उन्नत हो, ठीक तीन अवयवों पर बना होता है। इन्हें स्पष्ट रूप से समझिए; बाकी विवरण है।
| स्तंभ | सरल अर्थ | इमारत का उदाहरण |
|---|---|---|
| विनिर्देशन | “सही” का अर्थ क्या है, इसका सटीक कथन | “हर दरवाज़ा रात में बंद होना चाहिए” |
| सिस्टम | जाँची जा रही वास्तविक वस्तु (प्रोग्राम, सर्किट या प्रोटोकॉल) | इमारत और उसका लॉकिंग तंत्र |
| प्रमाण | कठोर तर्क कि सिस्टम हमेशा विनिर्देशन को पूरा करता है | “lock” दबाने से सभी दरवाज़े बंद होने का तार्किक प्रदर्शन |
और चौथा, शांत-सा अवयव पूरी चीज़ को विश्वसनीय बनाता है:
जिन proof assistants के नाम आप सुन सकते हैं, उनमें Lean, Rocq (पूर्व में Coq) और Isabelle शामिल हैं। वे, प्रभावी रूप से, असाधारण रूप से कठोर तर्क-जाँच इंजन हैं। हमारी आरंभिक कहानी में Zcash का प्रमाण Lean में लिखा गया था। उल्लेखनीय रूप से, आधुनिक AI मॉडल मनुष्यों के मार्गदर्शन में इन प्रमाणों को लिखने में तेजी से उपयोग किए जा रहे हैं, जिससे जिन प्रयासों में कभी वर्षों लगते थे वे हफ्तों में पूरे हो रहे हैं। मशीन फिर भी हर चरण जाँचती है, इसलिए गति बढ़ने से निश्चितता की कोई कीमत नहीं चुकानी पड़ती।
“प्रमाण” शब्द डरावना लग सकता है, इसलिए आइए एक ठोस, जाँचने योग्य उदाहरण से इसे सरल बनाते हैं। कोई क्रिप्टोग्राफी नहीं, केवल स्कूल का अंकगणित।
दावा: हर पूर्ण संख्या n के लिए, योग 0 + 1 + 2 + ... + n, n(n+1)/2 के बराबर होता है।
आप इसका परीक्षण कर सकते हैं। n = 5 से 0+1+2+3+4+5 = 15 मिलता है, और 5 × 6 / 2 = 15। ✓ यह मेल खाता है। n = 10 आज़माइए: योग 55 है, और सूत्र 10 × 11 / 2 = 55 देता है। ✓ (इनकी गणना और पुष्टि की गई है; वास्तव में यह दावा सीधे जाँचने पर 0 से 999 तक हर n के लिए सही है।)
लेकिन हज़ार मानों का परीक्षण भी “हर पूर्ण संख्या” तक नहीं पहुँचता। ऐसी संख्याएँ अनंत हैं। एक प्रमाण induction नामक तकनीक का उपयोग करके सीमित तर्क में उस अनंत अंतर को भर देता है:
n = 0 के लिए, योग केवल 0 है, और सूत्र 0 × 1 / 2 = 0 देता है। दोनों समान हैं। ✓k के लिए सही है। अब अगली संख्या, k+1, जोड़िए। k+1 तक का योग (sum up to k) + (k+1) = k(k+1)/2 + (k+1) है। बीजगणित की एक पंक्ति इसे (k+1)(k+2)/2 में पुनर्व्यवस्थित करती है, जो ठीक वही सूत्र है जिसमें k के स्थान पर k+1 है। ✓चूँकि यह शुरुआत (0) पर सही है और हर चरण इसे अगली संख्या तक ले जाता है, इसलिए यह सभी पूर्ण संख्याओं के लिए, हमेशा के लिए, एक सीमित तर्क में सही है। यही प्रमाण है। एक proof assistant बिल्कुल यही तर्क करता है, लेकिन यांत्रिक रूप से यह सत्यापित करता है कि “बीजगणित की एक पंक्ति” सहित हर चरण सचमुच पिछले चरण से निकलता है।
समझने योग्य छलाँग यह है: एक प्रमाण “अनंत मामलों” को एक सीमित, जाँचने योग्य तर्क में बदल देता है। यही वह महाशक्ति है जिसकी संरचनात्मक रूप से परीक्षण में कमी होती है।
औपचारिक सत्यापन आंशिक रूप से इसलिए शक्तिशाली है क्योंकि यह इस बात पर स्पष्टता देता है कि बग मूलतः कहाँ से आते हैं। किसी नियम-जाँच सिस्टम में हर दोष तीन में से एक स्थान तक पहुँचता है:
| बग का स्रोत | इसका अर्थ | क्या हम इसे सिद्ध करके दूर कर सकते हैं? |
|---|---|---|
| विनिर्देशन | गणित या नियम स्वयं गलत हैं (कोई शर्त छूटी हुई, कोई खराब परिभाषा) | हाँ, सीधे; यही औपचारिक सत्यापन का मुख्य क्षेत्र है |
| कार्यान्वयन | कोड सही विनिर्देशन को निष्ठापूर्वक लागू नहीं करता | आंशिक रूप से; अक्सर ऐसी विफलताएँ पहचानने योग्य साक्ष्य छोड़ती हैं |
| टूटी हुई धारणा | जिस चीज़ पर पूरा सिस्टम निर्भर है, वह असत्य निकलती है | नहीं; धारणाएँ अविभाज्य आधार हैं |
यह वर्गीकरण दिखने से अधिक महत्वपूर्ण है, और भाग 2 व 3 इसी पर आधारित हैं। सबसे गहरे और खतरनाक बग, जो हमेशा के लिए छिपे रह सकते हैं, आम तौर पर विनिर्देशन में होते हैं: सिस्टम को क्या करना चाहिए, इसका गणितीय विवरण। और विनिर्देशन ही वह चीज़ है जिसे machine-checked proof सीधे, सभी मामलों को एक साथ लेकर, जाँच सकता है। इसीलिए गंभीर औपचारिक-सत्यापन प्रयास पहले वहीं लक्ष्य रखते हैं।
औपचारिक सत्यापन शक्तिशाली है, लेकिन इसका वादा सटीक है, और इसे गलत समझना लोगों को भ्रमित करता है। इसलिए इसे सावधानी से कहें:
एक प्रमाण यह गारंटी देता है कि सिस्टम, बताई गई धारणाओं के अंतर्गत, विनिर्देशन को पूरा करता है। इससे अधिक कुछ नहीं।
इसके चार परिणाम हैं, और हर एक महत्वपूर्ण है:
औपचारिक सत्यापन को कमज़ोर करने के बजाय, यही सटीकता उसकी ताकत है। यह बताती है कि आपको ठीक-ठीक क्या मिल रहा है। जैसा कि हम भाग 3 में देखेंगे, Zcash टीम द्वारा अपने दायरे और धारणाओं को स्पष्ट रूप से बताना (“हमने इन नामित धारणाओं के अंतर्गत supply soundness सिद्ध की है, privacy नहीं”) उस ईमानदारी का आदर्श है।
इसे पठनीय बनाए रखने के लिए हमने सरलीकरण किया है। वास्तविक विनिर्देशन अंग्रेज़ी वाक्यों में नहीं, सटीक औपचारिक भाषाओं में लिखे जाते हैं; औपचारिक सत्यापन की कई शैलियाँ हैं (interactive theorem proving, model checking, SMT-based methods), जो अलग-अलग समस्याओं के लिए उपयुक्त हैं; और AI सहायता के साथ भी इन प्रमाणों को लिखना कुशलता व परिश्रम मांगने वाला काम बना हुआ है। हमने यह भी छोड़ दिया कि proof assistant आंतरिक रूप से तर्क को कैसे प्रदर्शित करता है। इनमें से कोई भी चीज़ मूल बात को नहीं बदलती: एक विनिर्देशन, एक सिस्टम, और बताई गई धारणाओं के अंतर्गत दोनों के मेल का machine-checked proof। आवश्यकता पड़ने पर विवरण वापस आएगा।
| शब्द | सरल अर्थ |
|---|---|
| Formal verification | गणितीय रूप से सिद्ध करना कि सिस्टम सभी मामलों के लिए किसी विनिर्देशन को पूरा करता है |
| Specification | “सही व्यवहार” का अर्थ क्या है, इसका सटीक कथन |
| System | जाँचा जा रहा वास्तविक प्रोग्राम, सर्किट या प्रोटोकॉल |
| Proof | सभी मामलों के लिए दावा स्थापित करने वाले तार्किक चरणों की सीमित श्रृंखला |
| Proof assistant / theorem prover | सॉफ़्टवेयर (Lean, Rocq, Isabelle) जो प्रमाण के हर चरण की जाँच करता है |
| Machine-checked | केवल मनुष्य द्वारा पढ़कर नहीं, बल्कि कंप्यूटर द्वारा चरण-दर-चरण सत्यापित |
| Induction | प्रमाण की तकनीक: शुरुआत में सही, और हर चरण इसे अगले चरण तक ले जाता है |
| Assumption | वह शर्त जिस पर प्रमाण निर्भर करता है; असत्य होने पर गारंटी लागू नहीं हो सकती |
क्या औपचारिक सत्यापन परीक्षण का स्थान ले लेता है? नहीं। दोनों एक-दूसरे के पूरक हैं। परीक्षण व्यावहारिक समस्याओं और गलत धारणाओं को सस्ते में पकड़ता है; सत्यापन बगों के ऐसे पूरे वर्गों को अस्वीकार करता है जिनका परीक्षण शायद कभी नमूना न ले।
यदि यह इतना शक्तिशाली है, तो हर चीज़ का औपचारिक सत्यापन क्यों नहीं किया जाता? यह महंगा है और विशेषज्ञ कौशल मांगता है, हालाँकि AI सहायता इसकी लागत घटा रही है। इसे उन सिस्टमों के लिए रखा जाता है जहाँ कोई दुर्लभ बग विनाशकारी हो सकता है, और ठीक वहीं इसकी लागत सार्थक होती है।
क्या औपचारिक रूप से सत्यापित सिस्टम फिर भी विफल हो सकता है? हाँ, यदि विनिर्देशन गलत था, कोई परिभाषा गलत लिखी गई थी, कोई धारणा सही नहीं निकली, या विफलता उस चीज़ से बाहर है जो निर्दिष्ट की गई थी। प्रमाण केवल उसी को कवर करता है जिसे वह कवर करने का दावा करता है।
क्या machine-checked proof मनुष्य के प्रमाण से अधिक विश्वसनीय होता है? बड़े और जटिल प्रमाणों के लिए, सामान्यतः हाँ। मशीन कोई सूक्ष्म कमी नहीं छोड़ेगी या अस्पष्ट तर्क स्वीकार नहीं करेगी, हालांकि वह फिर भी दिए गए विनिर्देशन और परिभाषाओं पर भरोसा करती है।
यदि AI प्रमाण लिखने में मदद करती है, तो उस पर भरोसा क्यों करें? क्योंकि proof assistant हर चरण को यांत्रिक रूप से जाँचता है। AI चरण प्रस्तावित करती है; मशीन उन्हें सत्यापित करती है। गलत चरण बस अस्वीकार हो जाता है, इसलिए AI गारंटी को कमज़ोर किए बिना कार्य को तेज़ करती है।
आप सिद्ध करते हैं कि किसी बैंक का सॉफ़्टवेयर “किसी खाते का balance कभी negative नहीं होने देता।” एक वर्ष बाद भी धन गायब होता रहता है। दोनों बातें एक साथ कैसे सही हो सकती हैं? (उत्तर नीचे है।)
प्रमाण ने ठीक एक गुण की गारंटी दी: balance कभी negative नहीं होगा। धन ऐसे तरीकों से गायब हो सकता है जिनसे यह गुण कभी संबंधित ही नहीं था, उदाहरण के लिए कोई बग जो धन को गलत (फिर भी non-negative) खाते में भेज देता है, या सिस्टम के ऐसे भाग में दोष जो कभी निर्दिष्ट ही नहीं था। सत्यापन ने ठीक वही किया जिसका उसने वादा किया था, और उससे अधिक कुछ नहीं। यह अनुभाग 6 की चेतावनी का प्रत्यक्ष उदाहरण है: प्रमाण विनिर्देशन को कवर करता है, “सही” की हर कल्पनीय धारणा को नहीं।
भाग 2 · Orchard बग: अब हम पूरी वास्तविक 2026 कहानी की ओर बढ़ते हैं। एक गोपनीयता सिस्टम ने cryptographic proofs का उपयोग कर राशियाँ छिपाईं, और उसके गणित की एक under-constrained पंक्ति का अर्थ था कि उन proofs को झूठ बोलने के लिए बनाया जा सकता था, जिससे असीमित अदृश्य नकली धन बन सकता था। हम देखेंगे कि “under-constrained circuit” का ठीक-ठीक अर्थ क्या है, इस प्रकार का बग हमेशा के लिए क्यों छिपा रह सकता है, और यह एक से अधिक बार क्यों हो चुका है।
ZecHub के लिए Formal Verification श्रृंखला का भाग।