Verifereum

KEVM, EVM का K-framework निष्पादन योग्य सिमेंटिक्स है: जब आपको अनुरूपता-सत्यापित निष्पादन, प्रतीकात्मक अन्वेषण, गैस तर्क, या ऐसे प्रमाणों की आवश्यकता हो जो इथेरियम के नियमों को बारीकी से ट्रैक करते हों, तो इसे बाइटकोड पर निर्देशित करें।

Kontrol, Foundry प्रॉपर्टी टेस्ट को KEVM-समर्थित प्रमाणों में बदल देता है, जिससे आप अकेले रॉ KEVM की तुलना में कम हस्तलिखित विनिर्देश कार्य के साथ औपचारिक गारंटी प्राप्त कर सकते हैं।

hax Rust के एक बड़े उपसमुच्चय को F* या Rocq जैसी औपचारिक भाषाओं में उच्च आश्वासन अनुवाद के लिए एक उपकरण है।

Act इथेरियम की एक घोषणात्मक विनिर्देश भाषा और टूलचेन है, जो किसी EVM प्रोग्राम के सभी व्यवहारों का वर्णन करती है ताकि SMT सॉल्वर, थ्योरम प्रूवर, या आर्थिक विश्लेषण उपकरण बाइटकोड-स्तर की शुद्धता और प्रोत्साहन संगतता के बारे में तर्क कर सकें, जिसमें ठोस कार्यान्वयन के विरुद्ध स्वचालित शोधन प्रमाण शामिल हैं।