सुरक्षा और परीक्षण

hax

औपचारिक सत्यापन

वेबसाइट cryspen/hax

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

संबंधित संसाधन

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

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

Verifereum

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