Anthropic का कहना है कि Claude ने 123 लाइब्रेरी में सुरक्षा गुणधर्मों को प्रमाणित किया

Anthropic ने 22 अक्टूबर, 2026 को शोध प्रकाशित किया, जिसमें बताया गया कि Theorem के साथ मिलकर किए गए एक प्रयास में Claude ने 123 ओपन-सोर्स लाइब्रेरी के 239 फ़ज़-परीक्षण एंट्री पॉइंट के लिए RISC-V असेंबली कोड स्तर पर सुरक्षा गुणधर्मों के मशीन-जाँचे गए औपचारिक प्रमाण तैयार किए।

Anthropic के अनुसार, Claude ने अपने पाए गए बग ठीक किए और फिर साबित किया कि हर 64 MB से छोटे इनपुट तथा Linux ऑपरेटिंग सिस्टम की हर मॉडल की गई प्रतिक्रिया और मेमोरी लेआउट के लिए प्रोग्राम हमेशा सामान्य रूप से समाप्त होंगे—न तो मेमोरी-सुरक्षा संबंधी त्रुटियाँ होंगी, न ही अभिकथन विफल होंगे। इन प्रमाणों में यह माना गया है कि प्रोग्राम Linux का उपयोग करने वाले RISC-V CPU पर, निश्चित मेमोरी बजट के साथ, सिंगल-थ्रेडेड स्टैटिक बाइनरी के रूप में चलता है। Anthropic ने बताया कि इन प्रमाणों में Rocq की लगभग 180 मिलियन पंक्तियाँ हैं। आम तौर पर, 18,000 RISC-V निर्देशों की माध्य लंबाई वाली बाइनरी को कवर करने वाले एक प्रमाण में लगभग 600,000 पंक्तियाँ होती हैं। कंपनी ने कहा कि उसकी जानकारी में, असेंबली कोड स्तर पर उत्पादन सॉफ़्टवेयर का औपचारिक सत्यापन करने के लिए AI का उपयोग करने का यह पहला बड़े पैमाने का प्रयास है।

इन प्रमाणों के एक हिस्से के साथ-साथ उनके पीछे के RISC-V और ऑपरेटिंग सिस्टम के अर्थ-विज्ञान को GitHub पर प्रकाशित किया जा रहा है। Anthropic ने कहा कि वह परियोजना के लिए बनाए गए उन विश्वसनीय घटकों को भी जारी कर रही है जो पहले से सार्वजनिक नहीं हैं, उन फ़ज़ परीक्षणों के पूरे प्रमाण भी जारी कर रही है जिनमें किसी सुधार की ज़रूरत नहीं पड़ी, और उन फ़ज़ परीक्षणों के विनिर्देश भी जारी कर रही है जिन्हें प्रमाणित नहीं किया जा सका। हालांकि, ऐसे प्रमाण जारी नहीं किए जा रहे जिनसे कोई ऐसा बग उजागर हो सकता है जिसे ठीक नहीं किया गया है।

फ़ज़ परीक्षणों को औपचारिक प्रमाणों में बदलना

इस तरीके में हर लाइब्रेरी के मौजूदा कंपाइल किए जा सकने वाले फ़ज़ परीक्षण को एक औपचारिक विनिर्देश में बदला जाता है, जिसमें एक नियम दर्ज होता है: 64 MB से छोटे किसी भी इनपुट पर परीक्षण क्रैश नहीं होता। यह विनिर्देश कंपाइल किए गए RISC-V निर्देशों पर आधारित है और इसमें RISC-V निर्देश समुच्चय तथा Linux प्रक्रियाओं के औपचारिक अर्थ-विज्ञान का उपयोग किया जाता है। इसके बाद Rocq प्रमाण-जाँचक हर पूरे किए गए प्रमाण को विनिर्देश के अनुरूप सत्यापित करता है। Anthropic का कहना है कि इससे केवल तीन घटक ऐसे रह जाते हैं जिन पर डेवलपरों को भरोसा करना होता है: RISC-V और Linux प्रक्रियाओं के औपचारिक मॉडल, प्रमेयों के सटीक कथन और स्वयं Rocq जाँचक।

Anthropic ने बताया कि उसने Google की OSS-Fuzz पहल में शामिल सैकड़ों परियोजनाओं पर यह प्रक्रिया लागू की। यह पहल पात्र ओपन-सोर्स परियोजनाओं के लिए लगातार फ़ज़ परीक्षण उपलब्ध कराती है और C तथा C++ प्रोग्रामों में AddressSanitizer को अपने आप जोड़ती है। यह ऐसा टूल है जो मेमोरी का अनुचित तरीके से उपयोग होने पर प्रोग्राम को क्रैश कर देता है। 22 अक्टूबर, 2026 के एक परिशिष्ट में प्रमाणित किए गए पूरे प्रमेय का विवरण दिया गया है: 64 MiB से छोटे सभी इनपुट और सभी मेमोरी लेआउट के लिए, न तो ASan से इंस्ट्रूमेंट की गई बाइनरी और न ही सामान्य बाइनरी में फ़ॉल्ट होता है, वे बीच में रुकती हैं या ऐसा व्यवहार दिखाती हैं जिसे मॉडल में शामिल नहीं किया गया है। दोनों के पढ़ने और लिखने के ट्रेस, समाप्त होने का व्यवहार और फ़ाइल सिस्टम की अंतिम स्थिति एक जैसी रहती है।

परिशिष्ट के अनुसार, इस प्रयास के दौरान Claude ने Rocq की लगभग एक अरब पंक्तियाँ लिखीं, जिनमें से लगभग 180 मिलियन पंक्तियाँ प्रमाण-जाँचक से जाँची गईं। cJSON के 391-पंक्तियों वाले पार्सर एंट्री पॉइंट के लिए 630,000 पंक्तियों का प्रमाण तैयार किया गया, जबकि fftw3 के लिए—जिसमें 51,000 पंक्तियाँ लिंक की गई थीं—480,000 पंक्तियों का प्रमाण तैयार किया गया। चूँकि प्रमाण पूरा करने से पहले Claude को कोड में सुधार करने की अनुमति थी, Anthropic ने सुधारों पर दंड लगाया, यह साबित करने के लिए अतिरिक्त श्रेय दिया कि किसी सुधार ने किन इनपुट को बदला, और पुरस्कार के तंत्र के दुरुपयोग को रोकने के लिए सुधारों का रिकॉर्ड रखा और उनका ऑडिट किया।

प्रमाण के प्रयासों के दौरान मिले बग

Anthropic के अनुसार, प्रमाणों के प्रयास में सैकड़ों बग सामने आए, जिनमें से कई ऐसे थे जिन्हें फ़ज़र शायद ही खोज पाता। एक लाइब्रेरी के एंट्री पॉइंट को प्रमाणित करते समय Claude ने एक डीकंप्रेसर में काउंटर अंडरफ़्लो पाया, जिससे सीमा से बाहर लिखने की समस्या हुई। यह समस्या केवल लगभग 20 MB के उन इनपुट पर होती थी जिनका लेआउट एक दुर्लभ, विशिष्ट रूप में था। अन्य खोजों में एक इमेज डिकोडर में सीमा से बाहर पढ़ने की समस्या शामिल थी, जिसके लिए 64 MB का इनपुट और 2 GB से अधिक मेमोरी चाहिए थी; एक ऐसी सीमा-बाह्य पठन समस्या, जिसके लिए एक ही फ़ाइल के दो हैंडल पर कॉल का एक खास क्रम आवश्यक था; और libexpat में CVE-2026-56132 की दोबारा खोज, जिसके लिए बहुत गहराई तक नेस्ट किया गया इनपुट चाहिए था।

Claude ने ऐसे तर्क-संबंधी बग भी खोजे जिनसे कभी क्रैश नहीं होता। इनमें इस बात पर लगी पाबंदी शामिल थी कि कोई ऐप्लिकेशन किन फ़ाइलों को लोड कर सकता है, जिसे हमेशा लागू नहीं किया जाता। Anthropic ने कहा कि कई व्यापक रूप से इस्तेमाल किए जाने वाले अहम ऐप्लिकेशन को सत्यापित करने के प्रयासों में एक ऐसा तर्क-संबंधी बग सामने आया जिसके बारे में पहले पता नहीं था और जो एक दशक से भी अधिक समय से मौजूद था। कंपनी ने यह भी बताया कि एक व्यापक रूप से इस्तेमाल किए जाने वाले PDF रीडर को सत्यापित करने के प्रयास के दौरान, उसे एक सप्ताह में उतने ही सुरक्षा बग मिले जितने की आम तौर पर एक साल में रिपोर्ट मिलती है।

अतिरिक्त प्रयोग और दक्षता से जुड़ी खोजें

OSS-Fuzz से आगे बढ़ते हुए, Anthropic ने Claude से RFC 1950 का औपचारिक विनिर्देश लिखने को कहा। यह तकनीकी दस्तावेज़ zlib संपीड़न प्रारूप को परिभाषित करता है। इसके बाद Claude को यह साबित करना था कि Linux कर्नेल में zlib का कार्यान्वयन इस विनिर्देश को सही ढंग से लागू करता है। Claude ने x86 के लिए कंपाइल की गई बाइनरी को सीधे प्रमाणित किया और इसके लिए x86 निर्देश समुच्चय का Claude द्वारा तैयार किया गया औपचारिक अर्थ-विज्ञान इस्तेमाल किया। Anthropic ने बताया कि उसने आधा दर्जन अन्य व्यापक रूप से इस्तेमाल की जाने वाली लाइब्रेरी के लिए भी यही प्रक्रिया दोहराई और उनमें मामूली, जिनका दुरुपयोग नहीं किया जा सकता ऐसे विशेष-स्थितियों वाले बग पाए, जिन्हें संबंधित अपस्ट्रीम परियोजनाओं में दर्ज किया जा रहा है। कंपनी ने यह भी बताया कि x86 अर्थ-विज्ञान तैयार करने के दौरान आधिकारिक संदर्भ दस्तावेज़ों में सैकड़ों और हार्डवेयर में इससे कम संख्या में त्रुटियाँ मिलीं। अर्थ-विज्ञान के माध्यम से निर्देशों को एक-एक करके चलाने पर Linux कर्नेल में Ubuntu यूज़रस्पेस को बूट किया जा सकता है।

एक अन्य प्रयोग में, Claude ने Rust में Python के एक बड़े उपसमुच्चय के लिए इंटरप्रेटर बनाया और Verus सत्यापन टूल की मदद से यह प्रमाणित किया कि वह एक अकादमिक शोधपत्र में बताई गई CPython की अर्थवत्ता का पालन करता है। तकनीकी परिशिष्ट के अनुसार, इंटरप्रेटर के सभी 17 स्तरों को प्रमाणित किया गया और यह प्रमेय स्थापित हुआ कि “जब भी इंटरप्रेटर कोई परिणाम देता है, तो वह वही परिणाम होता है जिसे औपचारिक अर्थवत्ता निर्धारित करती है।” Anthropic ने बताया कि Python के बेतरतीब ढंग से बनाए गए 1.7 मिलियन प्रोग्रामों पर अनुभवजन्य परीक्षण में, 99.95% परीक्षणों में उसका व्यवहार CPython जैसा ही पाया गया; जानबूझकर डाली गई सात गड़बड़ियों में से पाँच बेतरतीब परीक्षणों में पकड़ में नहीं आईं, जबकि सभी सात ने प्रमाण को अमान्य कर दिया।

दक्षता मापने के लिए, Anthropic ने OSS-Fuzz के वास्तविक एंट्री पॉइंट को छोटा करके सत्यापन के 36 छोटे कार्य बनाए। इससे 283–2,491 निर्देशों वाले प्रोग्राम बने, जिनके इनपुट 64 बाइट तक सीमित थे और जिनमें AddressSanitizer की जगह लगभग 100 निर्देशों वाला “mini-ASan” रनटाइम इस्तेमाल किया गया। Anthropic के अनुसार, Opus 5.5 इन कार्यों में से आधे को Opus 5 की तुलना में लगभग 40% कम टोकन में प्रमाणित करता है। Anthropic ने यह भी बताया कि साझा कार्यक्षेत्र में एक-दूसरे के प्रमाणों की नकल करने की अनुमति वाले एजेंटों को अकेले काम करने वाले एजेंटों की तुलना में 17% कम टोकन की जरूरत पड़ी; कुछ एजेंट पहले अकेले प्रयास में असफल होने के बाद सफल हुए, जबकि अकेले काम करने वाले एजेंट दो प्रमाण पूरे नहीं कर पाए। कंपनी ने कहा कि OSS-Fuzz प्रयास के दौरान बड़े पैमाने पर भी प्रमाणों के पुनः उपयोग का यही असर दिखा: एजेंट टीमों ने पूरे किए गए प्रमाणों की नकल की और उन्हें अपने काम के अनुरूप ढाला, क्योंकि हर प्रमाण का बड़ा हिस्सा साझा C रनटाइम और AddressSanitizer के आरंभीकरण कोड से संबंधित होता है।

बताई गई सीमाएँ और OSS Verify कार्यक्रम

Anthropic का कहना है कि इन प्रमाणों का यह अर्थ नहीं है कि लाइब्रेरी में कोई गड़बड़ी नहीं है: बची हुई गड़बड़ियाँ भरोसेमंद घटकों के भीतर या प्रमाणों के दायरे से बाहर हो सकती हैं। ये प्रमाण musl libc से जुड़ी एकल-थ्रेड वाली स्थिर RISC-V बाइनरी तक सीमित हैं, जबकि अधिकांश उपयोगकर्ता इन लाइब्रेरी को x86 या ARM पर चलाते हैं और glibc से गतिशील रूप से जोड़ते हैं। इसके अलावा, AddressSanitizer स्मृति-सुरक्षा से जुड़ी सभी गड़बड़ियों का पता नहीं लगाता। कंपनी ने कहा कि उसे उम्मीद है कि मॉडल बेहतर होने के साथ इन सीमाओं से निपटना संभव हो जाएगा।

Theorem अपने OSS Verify कार्यक्रम के ज़रिए पात्र ओपन-सोर्स परियोजनाओं को यही प्रक्रिया निःशुल्क उपलब्ध करा रहा है। कार्यक्रम में शामिल होने के लिए पुल अनुरोध के माध्यम से उसकी रिपॉज़िटरी में project.yaml, Dockerfile और build.sh फ़ाइलें जोड़ी जाती हैं। Theorem का कहना है कि वह OSS-Fuzz जैसी प्रक्रिया के तहत परियोजनाओं की समीक्षा करता है और व्यापक रूप से इस्तेमाल होने वाले महत्वपूर्ण बुनियादी ढाँचे को प्राथमिकता देता है। Theorem के अनुसार, अनुरक्षकों को Rocq कर्नेल द्वारा जाँचा गया ऐसा Rocq प्रमाण मिलता है कि हर फ़ज़ लक्ष्य 64 MiB तक के किसी भी इनपुट पर क्रैश नहीं होता। प्रमाण तैयार करने के दौरान मिलने वाली गड़बड़ियों की जानकारी अनुरक्षकों को ईमेल से निजी तौर पर दी जाती है और उन्हें सार्वजनिक करने की कोई समय-सीमा नहीं होती; प्रमाण तैयार करने में कई दिन लग सकते हैं। Theorem की योजना का लक्ष्य पूरे Nix इकोसिस्टम का सत्यापन करना है, जिसमें glibc, OpenSSL और cURL जैसे महत्वपूर्ण बुनियादी ढाँचे शामिल हैं।