वास्तव में सिद्ध क्या हुआ
एंथ्रोपिक की फ्रंटियर रेड टीम ने थियोरम के साथ मिलकर 22 अक्टूबर को उन परिणामों को प्रकाशित किया जो बड़े पैमाने पर औपचारिक सत्यापन के लिए क्लॉड के उपयोग के प्रयास से निकले। टीम ने गूगल के ओएसएस-फ़ज़ से मौजूदा फ़ज़ परीक्षण लिए, हर परीक्षण को ऐसी विशेषता माना जिसे कोड को पूरा करना चाहिए, उसे आरआईएससी-वी असेंबली में संकलित किया, और क्लॉड से मशीन द्वारा जाँचे जा सकने वाले प्रमाण लिखवाए कि परिणामी बाइनरी कभी क्रैश नहीं होती।
यह विशेषता सीमित और सटीक है: 64 एमबी से छोटे किसी भी इनपुट पर कार्यक्रम स्मृति-सुरक्षा त्रुटि या विफल अभिकथन के साथ क्रैश नहीं होगा। प्रमाण यह मानकर चलते हैं कि बाइनरी एकल-धागा और स्थैतिक है, स्मृति सीमा निश्चित है, और वह लिनक्स पर आरआईएससी-वी प्रोसेसर पर चल रही है; तथा वे रॉक प्रमाण-जाँचक, थियोरम की आरआईएससी-वी व लिनक्स प्रक्रिया अर्थ-व्याख्या, और नीचे के हार्डवेयर व ओकैमल संकलक पर भरोसा करते हैं।
आँकड़े
123 मुक्त-स्रोत लाइब्रेरियों में क्लॉड ने सिद्ध किया कि उस विनिर्देश के अंतर्गत 239 प्रवेश-बिंदु क्रैश से मुक्त हैं। प्रमाण कुल मिलाकर लगभग 18 करोड़ पंक्तियाँ रॉक कोड हैं। एक सामान्य प्रमाण लगभग 6,00,000 पंक्तियों का है, जबकि बाइनरी की माध्य लंबाई लगभग 18,000 आरआईएससी-वी निर्देश है। काम में कुछ सप्ताह लगे।
एंथ्रोपिक यह नहीं बताती कि कुल कितने प्रवेश-बिंदुओं पर प्रयास हुआ, इसलिए इन आँकड़ों से कोई सफलता दर नहीं निकलती। कंपनी का कहना है कि वह उन फ़ज़ परीक्षणों के प्रमाण प्रकाशित कर रही है जिनमें किसी पैच की ज़रूरत नहीं पड़ी, और उनके विनिर्देश जिन्हें वह सिद्ध नहीं कर सकी।
इस दौरान सैकड़ों बग सामने आए और क्लॉड ने उन्हें पैच किया, जिससे विनिर्देश फिर से बनते रहे। दिए गए उदाहरणों में एक डिकंप्रेसर में काउंटर अंडरफ़्लो है जो लगभग 20 एमबी इनपुट की दुर्लभ व्यवस्था पर ही सीमा-बाहर लेखन कराता है; एक छवि डिकोडर में सीमा-बाहर पठन है जिसके लिए 64 एमबी इनपुट और 2 जीबी से अधिक स्मृति चाहिए; और लिबएक्सपैट में सीवीई-2026-56132 की पुनः खोज है। एक मामला फ़ाइल-प्रतिबंध की ऐसी सुविधा का था जो हमेशा लागू नहीं होती थी: ऐसा तार्किक दोष जो कभी क्रैश नहीं कराता और एक दशक से अधिक समय से छिपा था।
स्पष्ट चोर रास्ता, और उसका इलाज
इस व्यवस्था में एक छेद है जिसका नाम टीम ने स्वयं लिया है। क्लॉड किसी प्रमेय को सिद्ध-योग्य बनाने के लिए कार्यक्रम को ही ऐसा लिख सकता था कि वह कभी क्रैश न हो। एंथ्रोपिक का कहना है कि उसने व्यवहार बदलने वाले पैच पर दंड लगाया, यह सिद्ध करने पर अतिरिक्त अंक दिए कि कोई पैच किन इनपुट को बदलता है, और हर पैच का लेखा रखकर उसकी जाँच की।
खुली समस्या लागत है
असली ओएसएस-फ़ज़ कोड से बने 36 छोटे सत्यापन कार्यों की कसौटी पर, जिनमें हर कार्य के लिए 50 लाख टोकन के बजट वाले तीन स्वतंत्र प्रयास थे, ओपस 5.5 ने आधे कार्य ओपस 5 की तुलना में लगभग 40% कम टोकन में सिद्ध किए। जिन एजेंटों को साझा कार्यक्षेत्र से एक-दूसरे के प्रमाण नक़ल करने की छूट थी, उन्होंने 17% कम टोकन लगाए और 36 में से 34 पूरे किए, जबकि अकेले काम करने वाले एजेंटों ने 32 पूरे किए।
एंथ्रोपिक सीमाओं के बारे में स्पष्ट है। «औपचारिक रूप से सत्यापित» का अर्थ दोष-मुक्त नहीं है: कोई प्रमाण-जाँचक यह पुष्टि नहीं कर सकता कि विनिर्देश वास्तविकता से मेल खाता है, और दोष विनिर्देश, मशीन-प्रतिरूप या भरोसेमंद आधार में बने रह सकते हैं। प्रमाण मसल से जुड़ी आरआईएससी-वी बाइनरियों को ढकते हैं, जबकि अधिकांश तैनातियाँ गतिशील रूप से जुड़ी ग्लिबसी के साथ x86 या एआरएम पर चलती हैं। और एक अकेले प्रमाण की लागत करोड़ों टोकन तक जा सकती है, जिसे कंपनी एक प्रमुख खुली समस्या कहती है।
अलग से, क्लॉड ने आरएफ़सी 1950 से एक विनिर्देश लिखा और सिद्ध किया कि लिनक्स कर्नेल का ज़िलिब कार्यान्वयन उसे x86 बाइनरी स्तर पर पूरा करता है। एंथ्रोपिक का कहना है कि उसने यही लगभग छह अन्य व्यापक रूप से प्रयुक्त लाइब्रेरियों पर दोहराया। यह x86 काम और आगे फैलता है या नहीं, यही देखने लायक़ है।
