Act

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

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

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.