مرکزی مواد پر جائیں
Verifereum
سیکیورٹی اور ٹیسٹنگ

Verifereum

رسمی تصدیق

سیکیورٹی · تعلیم · رسمی تصدیق

ویب سائٹ (نئے ٹیب میں کھلتا ہے)سوشل (نئے ٹیب میں کھلتا ہے)verifereum/verifereum(۵۱ ☆) (نئے ٹیب میں کھلتا ہے)

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

متعلقہ وسائل

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

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

hax

hax

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

Act

Act

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