Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

सुरक्षा · शिक्षा · एनालिटिक्स · औपचारिक सत्यापन · प्रतीकात्मक निष्पादन · डीबगिंग टूल · रनटाइम सत्यापन · Vyper

सोशल runtimeverification/evm-semantics(586 ☆)

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

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

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

hax

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

Act

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

Verifereum

Verifereum इथेरियम स्मार्ट कॉन्ट्रैक्ट्स को HOL4-समर्थित थ्योरम प्रूविंग से जोड़ता है ताकि जब स्वचालित SMT दृष्टिकोण पर्याप्त न हों, तो आप बहुत मजबूत शुद्धता के दावों का लक्ष्य रख सकें।