Security & testing

hax

Formal verification

رسمی تصدیق

ویب سائٹ cryspen/hax(۴۵۵ ☆)

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

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⁩ کے مقابلے میں کم ہاتھ سے لکھے گئے تصریحی کام کے ساتھ رسمی ضمانتوں کا پیچھا کر سکیں۔

Act

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

Verifereum

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