# الفاءپروف کوڈ اور سگنل: مشین کوڈ سیکیورٹی پروفز اور قابل اعتماد مفروضات کا معائنہ کیا گیا

Published: 2026-11-11

گوگل ڈیپ مائنڈ نے مرتب شدہ libsignal کمانڈ لائن ہارنس کے لیے منتخب سیکیورٹی خصوصیات کے مشین-چیک شدہ پروفز کی اطلاع دی ہے۔ لین پروف کو چیک کرتا ہے، جبکہ انسان تفصیلات اور اس کے مفروضات کو منظور کرتے ہیں۔ ایک علیحدہ کمپیریٹر منظور شدہ ہدف کے خلاف تھیورم اور تمام منحصر تعریفوں کو چیک کرتا ہے۔

Canonical: https://thedailydiff.dev/ur/video/2026-11-10-signal-machine-proof/

## اس ویڈیو میں کیا شامل ہے

- AI ایجنٹس امیدوار پروفز تیار کرتے ہیں؛ لین کا کرنل چیک کرتا ہے کہ آیا وہ انسانی-منظور شدہ رسمی دعوے کو قائم کرتے ہیں۔
- تصدیق شدہ ہدف ایک خاص مرتب شدہ libsignal CLI ہارنس ہے، جس میں قابل اعتماد سیمینٹکس اور کرپٹوگرافک معاہدے ہیں۔
- مرتب شدہ بائنری کو ثابت کرنے سے اس بائنری کی بیان کردہ خصوصیات کے لیے رسٹ کمپائلر کو قابل اعتماد بنیاد سے ہٹا دیا جاتا ہے۔
- محققین نے پہلے سے ٹھیک شدہ بگوں کی دو تنہائی میں دوبارہ تعارف کی اطلاع دی ہے جو ان کے علامتی سیکیورٹی تھیورم کی خلاف ورزی کرتے ہیں۔
- کمپیریٹر تھیورم اور ہر منحصر تعریف کو ایک محفوظ منظور شدہ تفصیلات کے خلاف چیک کرتا ہے؛ ترامیم ایک علیحدہ جائزہ شدہ عمل سے گزرتی ہیں۔

## سوالات و جوابات

### الفاپروف کوڈ نے سگنل کے نفاذ کے بارے میں کیا ثابت کیا؟

گوگل ڈیپ مائنڈ نے مرتب شدہ libsignal کمانڈ لائن ہارنس کے لیے منتخب سیکیورٹی خصوصیات کے چیک شدہ پروفز کی اطلاع دی ہے۔ تکنیکی کاغذ پیغام کی رازداری اور تصدیق کا احاطہ کرتا ہے، بیان کردہ ماڈلز کے تحت فارورڈ سیکریسی اور پوسٹ کمپرمائز سیکیورٹی کے ساتھ۔ نتیجہ حملہ آور، سیشن اور کرپٹوگرافک مفروضات پر شرائط کو برقرار رکھتا ہے۔ اس کا دائرہ کار ہر سگنل ایپلیکیشن یا انسٹالیشن کے لیے ایک عام ضمانت کو خارج کرتا ہے۔

### ایک AI سے تیار کردہ سیکیورٹی پروف کو کیا قائم کرنا چاہیے اس کا فیصلہ کون کرتا ہے؟

انسانی جائزہ لینے والے تفصیلات اور اس کے مفروضات کو منظور کرتے ہیں۔ گوگل ڈیپ مائنڈ کا تکنیکی کاغذ ایجنٹوں کو انسانی رہنمائی کے ساتھ تفصیلات کا مسودہ تیار کرنے اور جائزہ لینے والوں کو یہ ٹیسٹ کرنے کی وضاحت کرتا ہے کہ آیا بیانات بامعنی سیکیورٹی خصوصیات کو پکڑتے ہیں۔ لین نتیجے میں آنے والے پروف کی منطق کو چیک کرتا ہے۔ انسان ایک مضبوط ہدف کا انتخاب کرنے، مفروضات کا جائزہ لینے اور منظور شدہ تفصیلات میں مجوزہ تبدیلیوں کا فیصلہ کرنے کے لیے ذمہ دار رہتے ہیں۔

### رسٹ کمپائلر پر بھروسہ کرنے کے بجائے مرتب شدہ مشین کوڈ کی تصدیق کیوں کی جائے؟

مرتب شدہ بائنری کے بارے میں ایک پروف اس آرٹفیکٹ کے لیے بیان کردہ خصوصیات کو براہ راست قائم کرتا ہے۔ گوگل ڈیپ مائنڈ کا کاغذ بتاتا ہے کہ ایک کمپائلر ایرر جو ان خصوصیات میں سے کسی ایک کی خلاف ورزی کرتا ہے وہ تھیورم کو غلط کر دے گا۔ لہذا رسٹ کمپائلر اس دعوے کے لیے قابل اعتماد بنیاد کو چھوڑ دیتا ہے۔ پروف اب بھی انسٹرکشن ماڈل، لین کے کرنل اور بیان کردہ کرپٹوگرافک معاہدوں پر بھروسہ کرتا ہے۔

### کمپیریٹر ایک پروف ایجنٹ کو اپنے ہدف کو کمزور کرنے سے کیسے روکتا ہے؟

کمپیریٹر تھیورم اور ہر تعریف جس پر وہ منحصر ہے کا ایک محفوظ منظور شدہ تفصیلات کے خلاف موازنہ کرتا ہے۔ گوگل ڈیپ مائنڈ کا کاغذ کہتا ہے کہ پروف ایجنٹس اس محفوظ کاپی پر لکھ نہیں سکتے۔ چیکر اجازت شدہ محوروں کو بھی چیک کرتا ہے اور ایک تازہ کرنل میں پروف کو دوبارہ چلاتا ہے۔ مجوزہ تفصیلات کی ترامیم ایک علیحدہ جائزہ شدہ عمل کی پیروی کرتی ہیں، جبکہ انسان ہدف کی طاقت کے لیے ذمہ دار رہتے ہیں۔

### چیک شدہ پروف ورک فلو پر دی ڈیلی ڈف کا فیصلہ کیا تھا؟

دی ڈیلی ڈف کا فیصلہ SHIP IT تھا۔ نیکو چیک شدہ پروف ورک فلو کو بھیجے گا کیونکہ منظور شدہ دعویٰ جواب تیار کرنے والے ایجنٹ سے الگ رہتا ہے۔ وہ ہر نتیجے کے ساتھ دائرہ کار اور مفروضات کو منسلک رکھے گا۔ یہ ایپیسوڈ گوگل کے شائع شدہ پروف آرٹفیکٹ کی اطلاع دیتا ہے بغیر اسے آزادانہ طور پر دوبارہ بنائے اور ان شواہد کی حدود میں ورک فلو کو منظور کرتا ہے۔

## ابواب

- 0:00 ایک AI سیکیورٹی پروف کو کون چیک کرتا ہے؟
- 0:57 ایک دعویٰ ایک پروف ہدف کیسے بنتا ہے؟
- 1:39 مرتب شدہ بائنری کو کیوں ثابت کیا جائے؟
- 2:16 کون سی سیکیورٹی خصوصیات نفاذ کے خلاء سے بچ گئیں؟
- 2:59 کیا تفصیلات خراب کوڈ کو مسترد کر سکتی ہیں؟
- 3:36 کیا ایک صحیح پروف غلط سوال کا جواب دے سکتا ہے؟
- 4:13 ہدف کو متحرک ہونے سے کیا روکتا ہے؟
- 4:53 کیا میں یہ پروف ورک فلو بھیجوں گا؟

## ترجمہ شدہ ٹرانسکرپٹ

اصل انگریزی بیان سے ترجمہ کیا گیا۔ دستیاب آڈیو اور کیپشنز یوٹیوب کے زیر انتظام ہیں۔

### ایک AI سیکیورٹی پروف کو کون چیک کرتا ہے؟

0:00 ایک AI سیکیورٹی آڈٹ اب بھی ایک چیٹ بوٹ پر بھروسہ کرنے جیسا لگتا ہے۔ گوگل کے نئے سگنل کے نتیجے میں ریاضیاتی پروفز ہیں جو ایک علیحدہ کرنل چیک کرتا ہے۔ اس ویڈیو میں، گوگل نے کیا ثابت کیا؟ اور وہ ایک ایجنٹ کو اہداف کو تبدیل کرنے سے کیسے روکتے ہیں؟ یہ مفید جواب ہے۔ ماڈل امیدوار پروف لکھتے ہیں، اور لین پروفز کو ایک انسانی-منظور شدہ دعوے کے خلاف چیک کرتا ہے جو منتخب مرتب شدہ کوڈ کے بارے میں ہے۔ انسان اب بھی دعوے اور مفروضات کے مالک ہیں۔

0:21 آپ ماڈل کی فتح کی تقریر پر یقین کیے بغیر نتیجہ چیک کر سکتے ہیں۔ ایک علیحدہ چیک خاموشی سے سوال کو تبدیل کرنے کو پکڑتا ہے۔ ہم اسے تعریفوں تک فالو کریں گے۔ یہ منگل، دس نومبر ہے، اور یہ دی ڈیلی ڈف ہے۔ الفاپروف کوڈ انسانی رہنمائی کے ساتھ سافٹ ویئر کی تفصیلات لکھنے کے لیے گوگل کا فریم ورک ہے اور AI ایجنٹس کے ساتھ چیک شدہ پروفز تیار کرنا ہے۔ یہ مطالعہ libsignal کو ہدف بناتا ہے، جو سگنل کے میسجنگ کو نافذ کرنے والی رسٹ لائبریری ہے پروٹوکول، ایک خاص کمانڈ لائن پروگرام کے اندر۔

0:45 گوگل نے آج کام کا اعلان کیا۔ اس کے کاغذ میں کہا گیا ہے کہ پانچ محققین نے چار ہفتوں تک کام کیا۔ ایجنٹس نے پروف لکھے، جبکہ انسانوں نے اپنی زیادہ تر کوششوں کو تفصیلات پر صرف کیا۔ ضروریات نے مزید مہنگی میٹنگز بننے کا راستہ تلاش کر لیا ہے۔ تفصیلات بتاتی ہیں کہ پروگرام کو کیا کرنا چاہیے،

### ایک دعویٰ ایک پروف ہدف کیسے بنتا ہے؟

0:59 ایک حملہ آور کیا کنٹرول کرتا ہے، اور کن مفروضات کی دلیل کو ضرورت ہے۔ جائزہ لینے والے پوچھتے ہیں کہ کیا یہ اس سیکیورٹی کو پکڑتا ہے جس کی لوگوں کو پرواہ ہے۔ ایک کمزور سوال کا خوبصورتی سے چیک شدہ جواب اس سوال کو برقرار رکھتا ہے۔ ٹیم سگنل کے ہینڈ شیک اور اس کی میسج کی ریچٹ پر پہلے کی تحقیق پر مبنی ہے۔ رسمی تجزیات نے پہلے ہی ان ڈیزائنوں کا مطالعہ کیا تھا۔ گوگل کا دعویٰ ان کے سیکیورٹی دلائل کو ایک غیر ترمیم شدہ پروڈکشن لائبریری کے مرتب شدہ نفاذ سے جوڑتا ہے، جہاں ڈیزائن کو اصل کوڈ سے رابطہ برقرار رکھنا پڑتا ہے۔ سگنل کے چیف ٹیکنالوجی آفیسر، احرین کریٹ،

1:27 پہلے کی تصدیق کے چھوٹے دائرہ کاروں سے آگے ایک توسیع کی وضاحت کرتے ہیں۔ نفاذ کی تفصیلات میں آؤٹ آف آرڈر میسجز اور آرکائیو شدہ سیشنز شامل ہیں دیر سے آنے والے پیغامات کے لیے۔ اصل سافٹ ویئر ان رسیدوں کو رکھتا ہے جو آپ کے خوبصورت ڈائیگرام نے پھینک دیے۔ محققین غیر ترمیم شدہ رسٹ لائبریری کو معیاری

### مرتب شدہ بائنری کو کیوں ثابت کیا جائے؟

1:41 کمپائلر کے ساتھ ایک Arm 64 Linux ایگزیکیوٹیبل میں مرتب کرتے ہیں۔ ان کے تھیورم اس بائنری کو ایک رسمی انسٹرکشن ماڈل کا استعمال کرتے ہوئے بیان کرتے ہیں، ماخذ اور آپٹیمائزڈ مشین کوڈ کے درمیان خلاء کو پورا کرتے ہوئے پہنچتے ہیں۔ ایک کمپائلر ایرر جو ایک بیان کردہ خصوصیت کو توڑ دیتا ہے وہ اس کے تھیورم کو غلط کر دے گا۔ لہذا کمپائلر اس بائنری کے لیے قابل اعتماد بنیاد کو چھوڑ دیتا ہے۔ آپ اب بھی انسٹرکشن ماڈل اور لین کے چیکر پر بھروسہ کرتے ہیں۔ اعتماد کی حد منتقل ہو گئی، اور اس کا ایک پتہ ہے۔ تقریباً چھ اور نصف ملین لائنز پر مشتمل چیک شدہ پروف تقریباً چھبیس

2:06 ہزار قابل اعتماد تفصیلات اور انسٹرکشن-سیمینٹکس لائنوں پر مبنی ہیں۔ یہ آرٹفیکٹ کی گنتی ہے۔ انہیں انٹیلیجنس سکور کے طور پر سمجھنا ڈویلپرز کو ان کے نوڈ ماڈیولز فولڈر کے سائز سے درجہ بندی کرنے جیسا ہے۔

### کون سی سیکیورٹی خصوصیات نفاذ کے خلاء سے بچ گئیں؟

2:16 دلائل پیغام کی رازداری اور تصدیق کا احاطہ کرتے ہیں، بیان کردہ ماڈلز کے تحت فارورڈ سیکریسی اور پوسٹ کمپرمائز سیکیورٹی کے ساتھ۔ یہ آخری دو چوری شدہ کلید کے نقصان اور تازہ تبادلے کے بعد بحالی کی حدود کو بیان کرتے ہیں۔ ہر ضمانت میں حملہ آور اور سیشن کے لیے شرائط ہیں۔ کرپٹوگرافک پرائمیٹیوز قابل اعتماد معاہدوں کے پیچھے بیٹھے ہیں۔ پروف یہ فرض کرتا ہے کہ یہ روٹینز تفصیلات کے مطابق برتاؤ کرتی ہیں اور کرپٹوگرافک سیکیورٹی مفروضات پر انحصار کرتی ہیں۔ ایک پروف کرپٹوگرافی کو مثالی بناتا ہے؛ دوسرا حملہ آور کی کامیابی کی ممکنہ شرحوں کے بارے میں استدلال کرتا ہے۔

2:42 دونوں کے زیر بحث حالات پر پابندیاں ہیں۔ پوچھیں کہ کون سا بلڈ، کون سی پراپرٹی، اور کون سے مفروضات۔ یہ نتیجہ محققین کے کمانڈ لائن ہارنس سے متعلق ہے۔ گروپ میسجنگ مستقبل کا کام ہے، اور کمپیوٹیشنل ماڈل ملٹی ڈیوائس اسٹیٹ کو خارج کرتا ہے۔ ہر سگنل انسٹالیشن کو بگ فری کہنا تھیورم سے باہر بھٹکتا ہے۔ محققین نے پہلے سے ٹھیک شدہ دو سگنل بگوں کو

### کیا تفصیلات خراب کوڈ کو مسترد کر سکتی ہیں؟

3:02 الگ کاپیوں میں دوبارہ متعارف کرایا اور انہیں مرتب کیا۔ چیک شدہ پروفز نے دکھایا کہ وہ بائنریز علامتی سیکیورٹی تھیورم کی خلاف ورزی کرتی ہیں۔ اس نے ٹیسٹ کیا کہ کیا تفصیلات حقیقی خراب نفاذ کو مسترد کر سکتی ہیں۔ آپ کے سبز چیک مارک کو ایک سرخ ٹیسٹ کی ضرورت ہے۔ گوگل تفصیلات اور پروفز کو چیک کرنے کی ہدایات کے ساتھ شائع کرتا ہے۔ ریپوزیٹری کہتا ہے کہ ایک صاف بلڈ میں گھنٹے اور خاطر خواہ میموری لگتی ہے۔ اعلان کو پڑھنا لیپ ٹاپ پر کافی آسان ہے۔ ہارڈ ویئر ماڈل اور قابل اعتماد معاہدوں کو اب بھی جائزے کی ضرورت ہے۔

3:26 میں نے اس ایپیسوڈ کے لیے بڑا آرٹفیکٹ دوبارہ نہیں بنایا ہے۔ ہم شائع شدہ نتیجہ اور اس کی حدود کی اطلاع دے رہے ہیں۔ بیرونی افراد کے پاس اس کا معائنہ کرنے کا راستہ ہے، جو میرے لیے کسی اور AI فتح کے دور سے زیادہ اہم ہے۔ اب پھندا۔

### کیا ایک صحیح پروف غلط سوال کا جواب دے سکتا ہے؟

3:36 لین ایک ایسے بیان کا صحیح پروف قبول کر سکتا ہے جو تقریباً کچھ بھی نہیں مانگتا۔ ناممکن مفروضات ایک تھیورم کو بے کار بنا سکتے ہیں۔ ہیڈ لائن تھیورم کے نیچے دفن شدہ تعریف کو تبدیل کرنا ہدف کو کمزور کر سکتا ہے۔ کاغذ اس کے خلاف چیک ڈیزائن کرتا ہے۔ گیٹ کیپر ایک محفوظ منظور شدہ تفصیلات رکھتا ہے جسے پروف ایجنٹس لکھ نہیں سکتے۔ وہ ایک علیحدہ ترمیم کے عمل کے ذریعے اصلاحات تجویز کر سکتے ہیں۔ سیکیورٹی کمزوری کو ایک ممکنہ بگ کے طور پر بڑھا دیا جاتا ہے۔ پروور کی کامیابی کے اعلان کی یہاں کوئی اتھارٹی نہیں ہے۔

4:00 انسان قابل اعتماد مفروضات میں تبدیلیوں کا فیصلہ کرتے ہیں، براہ راست یا اپنی پالیسی کے ذریعے، اور ہر مہم کے بعد ترامیم کا جائزہ لیتے ہیں۔ ماہرانہ رائے برقرار رہتی ہے۔ ایجنٹ ایک مختلف اسائنمنٹ کی درخواست کر سکتا ہے۔ وہ خود کو پاسنگ گریڈ نہیں دے سکتا۔

### ہدف کو متحرک ہونے سے کیا روکتا ہے؟

4:13 یہ رہا وعدہ شدہ چیک۔ لین کا کمپیریٹر تھیورم اور ہر تعریف جس پر وہ منحصر ہے کا موازنہ کرتا ہے اس محفوظ منظور شدہ کاپی سے۔ یہ اجازت شدہ محوروں کو بھی چیک کرتا ہے اور ایک تازہ کرنل میں پروف کو دوبارہ چلاتا ہے۔ اس لیے ایک مددگار تعریف کو خاموشی سے کمزور کرنا اس چیز کو تبدیل کر دیتا ہے جس کا موازنہ کیا جا رہا ہے۔ ایک قبول شدہ پروف کو منظور شدہ ہدف کو قائم کرنا پڑتا ہے۔ یہ اب بھی انسانوں کو ایک مضبوط ہدف اور ایماندار مفروضات کا انتخاب کرنے کے لیے ذمہ دار ٹھہراتا ہے۔ اپنے AI ورک فلو کے لیے، قبولیت کے معیار کو

4:37 ورکر کے ترمیم کی اجازتوں سے باہر رکھیں اور مجوزہ تبدیلیوں کا علیحدہ جائزہ لیں۔ گوگل کا نتیجہ اس علیحدگی کو ٹھوس بناتا ہے۔ پروف لکھنے والا کام کرتا ہے؛ چیک کرنے کی حد فیصلہ کرتی ہے کہ آیا یہ گنا جاتا ہے۔ اگر آپ اسے سننے کے بجائے پڑھنا چاہتے ہیں تو، ڈیف ہر صبح آپ کے ان باکس میں آتا ہے، daily diff dot dev پر مفت، لنک نیچے ہے۔ تو آج کا فیصلہ SHIP IT ہے۔

### کیا میں یہ پروف ورک فلو بھیجوں گا؟

4:54 میں یہ چیک شدہ پروف ورک فلو بھیجوں گا کیونکہ منظور شدہ دعویٰ جواب تیار کرنے والے ایجنٹ سے الگ رہتا ہے۔ میں ہر نتیجے کے ساتھ دائرہ کار اور مفروضات کو منسلک رکھوں گا۔ سبسکرائب کریں، بیل کو دبائیں، اور مجھے تبصروں میں بتائیں کہ کیا آپ نے اسے مختلف طریقے سے مہر لگائی ہوتی۔ اور یہ آج کا ڈیف ہے۔ میں Axrisi سے نیکو ہوں۔ ذمہ داری سے ضم کریں۔

## ذرائع

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub