&Truth ने कोड के लिए सार्वभौमिक सत्यापन मशीन बनाने हेतु शुरुआती दौर में 70 मिलियन डॉलर जुटाए

&Truth, सॉफ्टवेयर सुरक्षित है या नहीं, यह गणितीय रूप से साबित करने वाली तकनीक विकसित करने वाली एक सार्वजनिक हित निगम, 29 अक्टूबर 2026 को अपना गुप्त काम सार्वजनिक करते हुए सामने आई। कंपनी ने शुरुआती दौर में जुटाई गई 70 मिलियन डॉलर की पूंजी और कोड के लिए अपनी ‘सार्वभौमिक सत्यापन मशीन’ बनाने की योजना का खुलासा किया।

अपनी शुरुआत की घोषणा में कंपनी ने बताया कि इसकी स्थापना 2026 की शुरुआत में हुई थी और इसे ऐसे समूह से शुरुआती दौर में 70 मिलियन डॉलर की पूंजी मिली, जिसे कंपनी ने एआई सुरक्षा और उद्यम पूंजी के क्षेत्र के अग्रणी लोगों का समूह बताया। कंपनी के अनुसार, उसकी सत्यापन मशीन किसी भी प्रोग्रामिंग भाषा में लिखे कोड को पढ़ने और गणितीय रूप से यह साबित करने के लिए बनाई जा रही है कि वह सुरक्षित, संरक्षित और सही है। इन प्रमाणों की स्वतंत्र रूप से कोई भी जाँच कर सकता है।

Lean पर आधारित प्रमाण स्वचालन

घोषणा के अनुसार, औपचारिक सत्यापन दशकों से मौजूद है, लेकिन पहले यह सीमित लोगों की पहुँच में था और महँगा पड़ता था, क्योंकि विशेषज्ञों को प्रमाण हाथ से तैयार करने होते थे। इस वजह से इसका इस्तेमाल केवल कुछ चुनिंदा महत्वपूर्ण प्रणालियों तक सीमित था। कंपनी ने कहा कि अब एआई औपचारिक प्रमाण तैयार करने के काम को 100 गुना या उससे अधिक तेज़ करता है और उसकी प्रमाण-स्वचालन तकनीक इस प्रक्रिया को 100 गुना और तेज़ कर देती है। इससे प्रमाण तैयार करने में लगने वाला समय वर्षों या महीनों से घटकर घंटों या मिनटों तक आ जाता है।

कंपनी ने अपनी उस तकनीक का भी ज़िक्र किया जिसे वह “विनिर्देश कारखाना” कहती है। उसके मुताबिक, यह तकनीक उद्यमों और डेवलपरों को मानवीय मंशा और व्यावसायिक आवश्यकताओं को बड़े पैमाने पर सटीक औपचारिक विनिर्देशों में बदलने में सक्षम बनाती है। इससे ऐसी गारंटियाँ मिलती हैं जिनकी स्वतंत्र रूप से जाँच की जा सकती है; वे परीक्षण या विक्रेता के दावों पर निर्भर नहीं होतीं।

&Truth, ओपन-सोर्स प्रमाण प्रणाली Lean और Mathlib पर काम कर रही है। Mathlib में गणितीय परिभाषाओं और प्रमेयों की 20 लाख से अधिक पंक्तियाँ हैं। कंपनी CSLib समेत अन्य ओपन-सोर्स तकनीकों का भी इस्तेमाल कर रही है। कंपनी के अनुसार, लक्ष्य सॉफ्टवेयर के लिए एक सार्वभौमिक औपचारिक शब्दावली तैयार करना है: प्रोग्रामिंग भाषाओं और प्रणालियों के गणितीय मॉडल, प्रमाण तकनीकें और ऐसे सटीक विनिर्देश, जिनसे अलग-अलग भाषाओं में स्वचालित सत्यापन संभव हो। &Truth ने कहा कि वह Lean Focused Research Organization के साथ काम करती है और अपनी आधारभूत लाइब्रेरी ओपन सोर्स के रूप में जारी करने का इरादा रखती है।

सह-संस्थापक और सह-सीईओ Clark Barrett ने कहा कि Lean और Mathlib ने एआई को गणित में तर्क करने के लिए एक सटीक भाषा दी, जबकि सॉफ्टवेयर के पास अब तक ऐसी कोई समकक्ष नींव नहीं थी। सह-संस्थापक और मुख्य विज्ञान अधिकारी Ilya Sergey ने कहा कि सॉफ्टवेयर पर भरोसा किसी कंपनी की बात पर नहीं, बल्कि ऐसे प्रमाण पर आधारित होना चाहिए जिसकी स्वतंत्र रूप से जाँच की जा सके।

संस्थापक और दोहरे मुख्यालय

Barrett Stanford University में कंप्यूटर विज्ञान के Corbel प्रोफेसर, Stanford Center for AI Safety के संस्थापक सह-निदेशक, Stanford Center for Automated Reasoning के निदेशक, CSLib के सह-निर्माता और स्वचालित तर्क इंजन cvc5 के परियोजना प्रमुख हैं। Sergey ने National University of Singapore में VERSE Lab की स्थापना की और ओपन-सोर्स सत्यापन टूल Veil तथा Velvet के सह-निर्माता रहे। सह-संस्थापक, सह-सीईओ और कार्यकारी अध्यक्ष Chris Hsu, Lean FRO Strategic Advisory Board के सदस्य और Infinitude Foundation के अध्यक्ष हैं। इससे पहले वे Kilometre Capital के सीईओ और Citadel Investment Group में प्रबंध निदेशक रह चुके हैं।

घोषणा में Gregory Malecha का भी नाम लिया गया, जिन्होंने पहले BlueRock Security में औपचारिक विधियों के काम का नेतृत्व किया था और BRiCk सत्यापन ढाँचे के प्रमुख वास्तुकार थे; Sebastian Ullrich, जो Lean 4 के सह-वास्तुकार और Lean Focused Research Organization के सह-संस्थापक हैं; Linus Lee, जो पहले Kilometre Capital में प्रबंध साझेदार थे; और Drew Harman, जो पहले Fastino Labs में मुख्य वाणिज्यिक अधिकारी तथा Insight Partners और Shasta Ventures में परिचालन साझेदार थे। &Truth ने कहा कि उसका काम Stanford University और National University of Singapore में औपचारिक सत्यापन तथा स्वचालित तर्क पर दशकों से हो रहे शोध पर आधारित है।

&Truth का अमेरिकी मुख्यालय Palo Alto में और अंतरराष्ट्रीय मुख्यालय Singapore में है। कंपनी ने कहा कि Singapore स्थित उसका कार्यालय अनुसंधान, इंजीनियरिंग, उत्पाद और बाज़ार-विस्तार से जुड़े कामों में उल्लेखनीय रूप से बढ़ेगा। घोषणा में Singapore के डिजिटल उद्योग के वरिष्ठ उपाध्यक्ष और सह-प्रमुख Low Jin Yong ने कहा कि यह मुख्यालय Singapore की भरोसे और सुरक्षा से जुड़ी क्षमताओं को बढ़ाएगा और विश्वसनीय एआई विकसित करने वाली कंपनियों के केंद्र के रूप में देश की स्थिति मजबूत करेगा।

कंपनी की वेबसाइट पर Lean के आविष्कारक और AWS के उपाध्यक्ष एवं विशिष्ट वैज्ञानिक Leonardo de Moura तथा Lean FRO Strategic Advisory Board के सदस्य और Google के विशिष्ट इंजीनियर Simone Severini के साथ एक गोलमेज़ चर्चा भी है।

साथ में प्रकाशित निबंधों में कंपनी के तर्क की विस्तृत चर्चा

29 अक्टूबर 2026 के एक साथ प्रकाशित निबंध में Hsu ने उन रुझानों का विस्तार से उल्लेख किया जिन्हें कंपनी सत्यापन को तत्काल आवश्यक बनाने वाला मानती है। उन्होंने Google के सीईओ Sundar Pichai के उस बयान का हवाला दिया कि Google में अब 75% नया कोड एआई तैयार करता है और इंजीनियर उसे मंज़ूरी देते हैं। उन्होंने Veracode के 2026 के परीक्षण का भी ज़िक्र किया, जिसमें पाया गया कि जिन कोडिंग कार्यों में सुरक्षा मायने रखती थी, उनमें एआई मॉडल लगभग आधे मामलों में विफल रहे। निबंध में सितंबर 2026 के एक अभियान का भी उल्लेख है, जिसमें एक हमलावर ने व्यापक रूप से इस्तेमाल होने वाले प्रिंट-प्रबंधन सॉफ्टवेयर की खामियों का फायदा उठाकर 48 देशों के 395 संगठनों में सेंध लगाने के लिए सैकड़ों एआई एजेंट तैनात किए थे। इसमें सितंबर 2026 में प्रकाशित सॉफ्टवेयर की रिकॉर्ड 14,959 कमजोरियों का भी ज़िक्र है—यह संख्या उससे एक साल पहले प्रकाशित कमजोरियों की संख्या से 3.5 गुना थी।

इस निबंध में औपचारिक सत्यापन की पहले की महत्वपूर्ण उपलब्धियों का उल्लेख है: seL4 माइक्रोकर्नेल के मूल प्रमाण को तैयार करने में विशेषज्ञों के लगभग 20 व्यक्ति-वर्ष लगे और इसमें करीब 8,700 पंक्तियों का कोड था; 2015 में, DARPA के HACMS कार्यक्रम के तहत, seL4 को Boeing के Unmanned Little Bird हेलिकॉप्टर में शामिल किया गया। कई हफ्तों तक पहुँच दिए जाने के बावजूद, एक पेशेवर रेड टीम उसके उड़ान नियंत्रणों में सेंध नहीं लगा सकी। इसके अलावा, सितंबर 2026 में Anthropic के विकसित एक एआई मॉडल ने 11 दिनों में Lean में फ़र्मा के अंतिम प्रमेय का पूरा प्रमाण औपचारिक रूप दिया। निबंध यह भी बताता है कि 2026 की शुरुआत में Lean FRO के वरिष्ठ अनुसंधान सॉफ्टवेयर इंजीनियर Kim Morrison ने Anthropic के Claude का इस्तेमाल करते हुए, बहुत कम मानवीय मार्गदर्शन के साथ, Lean में zlib कंप्रेशन लाइब्रेरी का एक संस्करण बनाया और यह सिद्ध किया कि वह हमेशा उसी डेटा को हूबहू बहाल करती है जिसे उसने कंप्रेस किया था।

निबंध में Lean के निर्माता Leonardo de Moura का यह कथन उद्धृत है: “परीक्षण से भरोसा मिलता है। प्रमाण गारंटी देता है।”

29 अक्टूबर, 2026 को प्रकाशित एक दूसरे निबंध में Sergey प्रोग्राम सत्यापन की कार्यप्रणाली समझाते हैं। इसकी शुरुआत Alan Turing के 1949 के शोधपत्र “Checking a Large Routine” से होती है, जिसमें प्रस्ताव दिया गया था कि प्रोग्रामर अपने कोड के साथ सटीक दावे भी दें, ताकि जाँचकर्ता हर दावे को अलग-अलग सत्यापित कर सके। निबंध में विनिर्देशों, लूप इनवेरिएंट और Lean में जाँचे गए प्रमाणों का वर्णन है। इसमें कहा गया है कि &Truth का लक्ष्य डेवलपरों को स्वतंत्र रूप से जाँचे जा सकने वाले साक्ष्य—जैसे Lean में औपचारिक प्रमाण—ऐसी लागत पर उपलब्ध कराना है कि सत्यापन विकास प्रक्रिया का नियमित हिस्सा बन सके।

&Truth अपनी दीर्घकालिक परिकल्पना को “वाइब-कोडिंग” से “सत्यापन-कोडिंग” की ओर बदलाव के रूप में पेश करता है। इसमें एआई से तैयार कोड को लागू करने से पहले गणितीय रूप से सत्यापित किया जाता है, एआई एजेंट ऐसे परिवेशों में काम करते हैं जिनकी सीमाएँ प्रमाणित हों, पुराने सॉफ्टवेयर का सुरक्षित आधुनिकीकरण किया जाता है और महत्वपूर्ण बुनियादी ढाँचे को स्वतंत्र रूप से जाँची जा सकने वाली गणितीय गारंटियों से सुरक्षित रखा जाता है।