Vitalik Buterin: AI کی مدد سے رسمی تصدیق محفوظ سافٹ ویئر ڈویلپمنٹ کا مستقبل ہے

مندرجات کا جدول Vitalik Buterin نے سائبر سیکیورٹی کے مستقبل کے لیے ایک پرامید کیس پیش کیا ہے، یہ دلیل دیتے ہوئے کہ AI کی مدد سے باضابطہ تصدیق بنیادی طور پر اس بات کو تبدیل کر سکتی ہے کہ کس طرح محفوظ سافٹ ویئر لکھا جاتا ہے۔ AI کو کوڈ سیکیورٹی کے لیے خطرہ کے طور پر دیکھنے کے بجائے، Buterin اسے ایک ایسے ٹول کے طور پر دیکھتا ہے جو رسمی تصدیق کے ساتھ جوڑ کر، ریاضی کے اعتبار سے ثابت شدہ، انتہائی موثر سافٹ ویئر تیار کر سکتا ہے۔ اس کا نقطہ نظر AI سے چلنے والے سائبر حملوں کے بارے میں صنعت میں بڑھتی ہوئی مایوسی کو چیلنج کرتا ہے۔ سافٹ ویئر کی ترقی کے لئے ایک نیا نقطہ نظر Ethereum تحقیقی حلقوں کے اندر کرشن حاصل کر رہا ہے. ڈویلپرز کم درجے کی زبانوں میں یا براہ راست لین میں کوڈ لکھ رہے ہیں، ایک ایسی زبان جو قابل تصدیق ریاضیاتی ثبوتوں کے لیے استعمال ہوتی ہے۔ مقصد وہ کوڈ ہے جس کی درستگی خود بخود اور ریاضی سے جانچی جا سکتی ہے۔ Buterin اس طریقہ کو ممکنہ طور پر تبدیلی کے طور پر بیان کرتا ہے، محقق یوچی ہیرائی کا حوالہ دیتے ہوئے، جو اسے "سافٹ ویئر کی ترقی کی آخری شکل" کہتے ہیں۔ نقطہ نظر کارکردگی کو مکمل طور پر پڑھنے کی اہلیت سے الگ کرتا ہے۔ کوڈ کا ایک ورژن تیزی سے چلتا ہے۔ دوسرا واضح طور پر انسانی سمجھ کے لیے لکھا گیا ہے، اور ایک ثبوت ان کو جوڑتا ہے۔ یہ خاص طور پر ZK-EVMs، کوانٹم مزاحم دستخط، اور متفقہ الگورتھم جیسے ہائی اسٹیک سسٹمز کے لیے اہمیت رکھتا ہے۔ یہ سسٹم بنانے کے لیے پیچیدہ ہیں لیکن ان میں حفاظتی خصوصیات ہیں جو کہ رسمی طور پر بیان کرنے کے لیے سیدھی ہیں۔ پیچیدگی اور وضاحت کے درمیان وہ فرق بالکل وہی ہے جہاں رسمی تصدیق بہترین کارکردگی کا مظاہرہ کرتی ہے۔ Arklib اور evm-asm جیسے پروجیکٹس پہلے سے ہی اس طریقہ کو Ethereum انفراسٹرکچر پر لاگو کر رہے ہیں۔ evm-asm پروجیکٹ RISC-V اسمبلی میں براہ راست EVM عمل درآمد کرتا ہے، پھر باضابطہ طور پر ثابت کرتا ہے کہ یہ پڑھنے کے قابل اعلی سطحی ورژن سے میل کھاتا ہے۔ صنعت میں کچھ آوازوں نے دلیل دی ہے کہ AI سے چلنے والے بگ کی دریافت محفوظ، بے اعتماد سافٹ ویئر کو ناممکن بنا دیتی ہے۔ بہت سے لوگوں نے دعویٰ کیا ہے کہ AI کی مدد سے بگ ڈھونڈنا، محفوظ کوڈ (اور اس وجہ سے کوئی بھی چیز بے اعتبار) ناممکن ہو جائے گی۔ میرے پاس بہت زیادہ پر امید نظر ہے، اور AI کی مدد سے باضابطہ توثیق اس وجہ کا ایک بڑا حصہ ہے کیوں:https://t.co/0ceMBZ6uqj — vitalik.eth (@VitalikButerin) 18 مئی 2026 Buterin اس نقطہ نظر کو براہ راست پیچھے دھکیلتا ہے۔ وہ موجودہ دور کو حملہ آوروں کے حق میں مستقل تبدیلی کے بجائے ایک عبوری چیلنج کے طور پر تیار کرتا ہے۔ ایک بار زمین کی تزئین کی ترتیب کے بعد، اس کا خیال ہے کہ دفاع پہلے سے زیادہ مضبوط ہو جائے گا. وہ معاون ثبوت کے طور پر موزیلا کے کام کی طرف اشارہ کرتا ہے۔ موزیلا نے نوٹ کیا ہے کہ حفاظتی نقائص محدود ہیں اور محافظوں کے پاس اب ان سب کو تلاش کرنے کا ایک حقیقت پسندانہ راستہ ہے۔ سائپرپنک روایت، اس خیال پر بنائی گئی ہے کہ ڈیجیٹل محافظوں کو فائدہ ہوتا ہے، اسے ترک کرنے کی ضرورت نہیں ہے۔ Buterin کا ​​ماڈل سافٹ ویئر کو ایک بھروسہ مند محفوظ کور اور کم قابل بھروسہ کنارے والے اجزاء میں تقسیم کرتا ہے۔ کنارے کم سے کم اجازتوں کے ساتھ سینڈ باکس میں چلتا ہے۔ کور، جان بوجھ کر چھوٹا رکھا گیا ہے، AI کی مدد سے رسمی تصدیق کا پورا فائدہ حاصل کرتا ہے۔ بٹرین محتاط ہے کہ باضابطہ تصدیق کے لیے کیس کو زیادہ نہ سمجھا جائے۔ کئی دستاویزی ناکامیاں اس کی حقیقی حدود کو ظاہر کرتی ہیں۔ کیڑے باضابطہ طور پر تصدیق شدہ C مرتب کرنے والوں میں نمودار ہوئے ہیں جہاں کچھ رکاوٹوں کی وضاحت نہیں کی گئی تھی۔ libcrux میں 2025 کی کمزوری نے ظاہر کیا کہ غیر تصدیق شدہ اندرونی ریپر مخصوص ہارڈویئر پلیٹ فارمز پر آؤٹ پٹ کو خراب کر سکتے ہیں۔ تصدیق شدہ حصے سے باہر کوڈ میں غیر ہینڈل ڈکرپشن کی خرابی کی وجہ سے ایک اور بگ نے عمل کریش کر دیا۔ ناکامیوں کے درمیان پیٹرن مطابقت رکھتا ہے: یا تو کوڈ کے صرف ایک حصے کی تصدیق کی گئی تھی، یا ایک اہم خاصیت کو کبھی بھی ثبوت میں شامل نہیں کیا گیا تھا۔ رسمی تصدیق سافٹ ویئر کو لفظ کے مکمل انسانی معنوں میں درست ثابت نہیں کر سکتی، صرف وہی مخصوص خصوصیات مخصوص مفروضوں کے تحت رکھتی ہیں۔ سائیڈ چینل حملے ایک اور حد پیش کرتے ہیں۔ یہاں تک کہ ایک مکمل طور پر ثابت شدہ انکرپشن سکیم بھی برقی اتار چڑھاو کے ذریعے نجی کلید کو لیک کر سکتی ہے۔ حملہ آوروں کے ریاضیاتی ماڈل ہمیشہ ہر حقیقی دنیا کے رساو کی قسم کو نہیں پکڑتے ہیں۔ بٹرین کا نتیجہ ماپا جاتا ہے۔ رسمی توثیق ایک مکمل حل نہیں ہے، لیکن یہ پہلے سے جاری حفاظتی رجحان کے لیے ایک طاقتور سرعت ہے - جسے AI نمایاں طور پر زیادہ قابل رسائی بناتا ہے۔