Anthropic का कहना है कि Claude ने औपचारिक प्रमाणों से साबित किया कि 123 ओपन-सोर्स लाइब्रेरी क्रैश नहीं हो सकतीं

Theorem के साथ सहयोग में, Anthropic का कहना है कि उसने Claude का उपयोग करके 100 से अधिक वास्तविक दुनिया की ओपन-सोर्स लाइब्रेरी में असेंबली स्तर (RISC-V) पर सुरक्षा गुणों को साबित किया। कंपनी इसे इस स्तर पर प्रोडक्शन सॉफ़्टवेयर का औपचारिक सत्यापन करने में AI के पहले बड़े पैमाने के इस्तेमाल के रूप में बताती है।

Anthropic के अनुसार:

• क्या साबित किया गया: 123 OSS-Fuzz लाइब्रेरी में 239 fuzz-test एंट्री पॉइंट के लिए, 64 MB से कम के हर इनपुट पर प्रोग्राम सामान्य रूप से समाप्त होते हैं—उनमें न तो मेमोरी-सुरक्षा संबंधी त्रुटियाँ होती हैं और न ही assertions विफल होते हैं। यह इन मान्यताओं के तहत लागू होता है: एक निश्चित मेमोरी बजट वाला सिंगल-थ्रेडेड static binary, जो Linux चलाने वाले RISC-V CPU पर हो। इन प्रमाणों में कुल लगभग 180 मिलियन पंक्तियों का Rocq कोड है, जिन्हें Rocq proof checker ने जाँचा।
• कैसे: हर लाइब्रेरी के मौजूदा fuzz test को एक विनिर्देश में बदला गया ("यह test कभी क्रैश नहीं होता"), और Claude ने रास्ते में मिली गड़बड़ियों को ठीक करते हुए उसका प्रमाण लिखा। Anthropic का कहना है कि इससे सैकड़ों बग मिले, जिनमें ऐसे बग भी शामिल हैं जिन तक fuzzing से पहुँचना मुश्किल होता—जैसे एक ऐसा out-of-bounds write जिसके लिए 20 MB का दुर्लभ इनपुट चाहिए, और libexpat में CVE-2026-56132 का दोबारा पता लगना।
• अन्य प्रयोग: Claude ने साबित किया कि Linux kernel का zlib कार्यान्वयन x86 binary स्तर पर RFC 1950 के विनिर्देश से मेल खाता है, और एक Rust Python interpreter बनाया जिसका व्यवहार 1.7 मिलियन यादृच्छिक प्रोग्रामों में 99.95% मामलों में CPython से मेल खाता था। Anthropic यह भी कहता है कि व्यापक रूप से इस्तेमाल किए जाने वाले एक PDF reader पर औपचारिक-सत्यापन के प्रयासों में एक सप्ताह में उतने सुरक्षा बग मिले, जितने आम तौर पर एक साल में रिपोर्ट होते हैं।
• लागत: प्रमाण तैयार करने में सैकड़ों मिलियन tokens लग सकते हैं। 36 छोटे सत्यापन कार्यों पर, Anthropic का कहना है कि Opus 5.5 उनमें से आधे को Opus 5 की तुलना में लगभग 40% कम tokens में साबित करता है, और प्रमाण साझा करने वाले agents को 17% कम tokens की ज़रूरत पड़ी।

Anthropic इन प्रमाणों के एक हिस्से और RISC-V तथा Linux semantics को प्रकाशित कर रहा है। Theorem अन्य ओपन-सोर्स प्रोजेक्ट के लिए यही प्रक्रिया चलाने की पेशकश करता है और अपना कोड सत्यापित करने के लिए Claude skill प्रकाशित कर रहा है। Anthropic ध्यान दिलाता है कि इससे यह साबित नहीं होता कि लाइब्रेरी में कोई बग नहीं है: बाकी बग भरोसेमंद घटकों में या प्रमाणों के दायरे से बाहर हो सकते हैं।