K Semantics of the Ethereum Virtual Machine (EVM)

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.

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

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