Security & testing

Act

Formal verification

تعلیم · تجزیات · رسمی تصدیق · علامتی عمل درآمد

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

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

⁦KEVM⁩ ⁦EVM⁩ کی ⁦K-framework⁩ ایگزیکیوٹیبل سیمینٹکس ہے: جب آپ کو کنفارمنس چیک شدہ ایگزیکیوشن، علامتی کھوج، گیس کی استدلال، یا ایسے ثبوتوں کی ضرورت ہو جو ایتھیریم کے اصولوں کو قریب سے ٹریک کرتے ہوں تو اسے بائٹ کوڈ پر پوائنٹ کریں۔

Kontrol - formal verification tool based on Foundry and KEVM

⁦Kontrol⁩ ⁦Foundry⁩ پراپرٹی ٹیسٹس کو ⁦KEVM⁩ کے حمایت یافتہ ثبوتوں میں تبدیل کرتا ہے تاکہ آپ صرف خام ⁦KEVM⁩ کے مقابلے میں کم ہاتھ سے لکھے گئے تصریحی کام کے ساتھ رسمی ضمانتوں کا پیچھا کر سکیں۔

hax

⁦hax⁩ ⁦Rust⁩ کے ایک بڑے سب سیٹ کو فارمل زبانوں جیسے ⁦F*⁩ یا ⁦Rocq⁩ میں ہائی ایشورنس ٹرانسلیشنز کے لیے ایک ٹول ہے۔

Verifereum

⁦Verifereum⁩ ایتھیریم سمارٹ کنٹریکٹس کو ⁦HOL4⁩ کی حمایت یافتہ تھیورم پرونگ سے جوڑتا ہے تاکہ جب خودکار ⁦SMT⁩ طریقے کافی نہ ہوں تو آپ انتہائی مضبوط درستگی کے دعووں کا ہدف بنا سکیں۔