hax

KEVM हे EVM चे K-framework एक्झिक्युटेबल सिमेंटिक्स आहे: जेव्हा तुम्हाला कन्फॉर्मन्स-चेक्ड एक्झिक्युशन, सिम्बॉलिक एक्सप्लोरेशन, गॅस रिझनिंग, किंवा इथेरियमच्या नियमांचा बारकाईने मागोवा घेणाऱ्या पुराव्यांची आवश्यकता असते, तेव्हा त्याला बाइटकोडवर निर्देशित करा.

Kontrol Foundry प्रॉपर्टी चाचण्यांना KEVM-समर्थित पुराव्यांमध्ये रूपांतरित करते, जेणेकरून तुम्ही केवळ रॉ KEVM च्या तुलनेत कमी हाताने लिहिलेल्या स्पेसिफिकेशनच्या कामासह औपचारिक हमी मिळवू शकाल.

Act ही इथेरियमची डिक्लेरेटिव्ह स्पेसिफिकेशन भाषा आणि टूलचेन आहे जी EVM प्रोग्रॅमच्या सर्व वर्तनांचे वर्णन करते, जेणेकरून SMT सॉल्व्हर्स, थिअरम प्रूव्हर्स किंवा आर्थिक विश्लेषण साधने बाइटकोड-स्तरीय अचूकता आणि इन्सेंटिव्ह कम्पॅटिबिलिटीबद्दल तर्क करू शकतील, ज्यामध्ये काँक्रीट इम्प्लिमेंटेशन्सच्या विरुद्ध स्वयंचलित रिफाइनमेंट प्रूफ्स्चा समावेश आहे.