سیکیورٹی اور ٹیسٹنگ

Certora AutoProver

رسمی تصدیق

رسمی تصدیق · تصدیق

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

متعلقہ وسائل

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

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

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

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

Verifereum

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

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.