हलमोस के साथ प्रतीकात्मक परीक्षण: औपचारिक सत्यापन के लिए मौजूदा परीक्षणों का लाभ उठाना

औपचारिक सत्यापन - किसी भी संख्या में इनपुट पर किसी प्रोग्राम या स्मार्ट अनुबंध का "निरीक्षण" करने के लिए गणितीय तरीकों का उपयोग करने की प्रक्रिया - आमतौर पर उच्च गुणवत्ता, अधिक सुरक्षित कोड लिखने के लिए पारंपरिक परीक्षण के अधिक संक्षिप्त, अधिक व्यापक विकल्प के रूप में देखी जाती है। लेकिन वास्तव में, औपचारिक सत्यापन एक खुली और इंटरैक्टिव प्रक्रिया है। यूनिट परीक्षण की तरह, डेवलपर्स को औपचारिक विशिष्टताओं को गतिशील रूप से परिभाषित और परत करना चाहिए, जैसे-जैसे उनका कोड और विश्लेषण विकसित होता है, उनके दृष्टिकोण को दोहराते रहना चाहिए। इसके अलावा, औपचारिक सत्यापन केवल इसके विनिर्देशों जितना ही प्रभावी है, जिसे लिखने में समय लग सकता है (और अक्सर सीखने की तीव्र अवस्था के साथ आता है)। 

कई डेवलपर्स के लिए जो प्रक्रिया को कठिन पाते हैं, किसी प्रोग्राम की शुद्धता का पता लगाने के लिए यूनिट परीक्षण अक्सर अधिक लागत प्रभावी और समय-कुशल मार्ग होते हैं। व्यवहार में, औपचारिक सत्यापन इकाई परीक्षण का अधिक व्यापक विकल्प नहीं है, बल्कि एक पूरक है। इन प्रक्रियाओं की अलग-अलग ताकत और सीमाएँ हैं, जो एक साथ उपयोग किए जाने पर और भी अधिक आश्वासन प्रदान करती हैं। डेवलपर्स को हमेशा यूनिट परीक्षण लिखने की आवश्यकता होगी - तो क्या होगा यदि हम औपचारिक सत्यापन के लिए समान गुणों का उपयोग कर सकें?

हेल्मोस, हमारा खुला स्रोत औपचारिक सत्यापन उपकरण, डेवलपर्स को इसकी अनुमति देता है पुनः प्रयोग प्रतीकात्मक परीक्षण के माध्यम से औपचारिक विशिष्टताओं के लिए इकाई परीक्षणों के लिए समान गुण लिखे गए। शुरू से ही संपत्तियों का एक मजबूत सेट बनाने के बजाय, डेवलपर्स दोहराव वाले काम से बच सकते हैं और शुरुआत से शुरू किए बिना एक समय में कुछ विशिष्टताओं के परीक्षण में सुधार कर सकते हैं। हमने इस टूल को औपचारिक सत्यापन प्रक्रिया में अन्य उपकरणों के साथ-साथ औपचारिक सत्यापन के लिए ऑन-रैंप के रूप में उपयोग के लिए डिज़ाइन किया है; डेवलपर्स प्रक्रिया में बाद में और अधिक जोड़ने से पहले, न्यूनतम प्रयास के साथ कुछ विश्लेषणों के साथ शुरुआत कर सकते हैं।

इस पोस्ट में, हम औपचारिक सत्यापन की चुनौतियों और प्रतीकात्मक परीक्षण के साथ इकाई परीक्षण और औपचारिक सत्यापन के बीच अंतर को पाटने की क्षमता को कवर करते हैं। फिर हम मौजूदा स्मार्ट कॉन्ट्रैक्ट कोड का उपयोग करके हेल्मोस के डेमो के माध्यम से चलते हैं, और डेवलपर्स के लिए उपलब्ध अन्य औपचारिक सत्यापन टूल (कई खुले स्रोत) पर एक त्वरित नज़र डालते हैं।

औपचारिक सत्यापन बनाम परीक्षण

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

औपचारिक सत्यापन की तरह, इकाई परीक्षण में यह मूल्यांकन करना शामिल है कि कोई प्रोग्राम अपेक्षा के अनुरूप काम करता है या नहीं; हालाँकि, परीक्षण केवल प्रोग्राम के व्यवहार की जाँच करता है कुछ इनपुट, जबकि औपचारिक सत्यापन इसकी जाँच कर सकता है सब संभावित इनपुट. परीक्षण और औपचारिक सत्यापन दोनों के लिए कार्यक्रम के अपेक्षित व्यवहार के विवरण की आवश्यकता होती है (परीक्षण में उपयोग किए जाने वाले परीक्षण मामलों और औपचारिक सत्यापन में उपयोग किए जाने वाले औपचारिक विनिर्देशों के साथ)। लेकिन, जब एक साथ उपयोग किया जाता है, तो वे किसी कार्यक्रम की अधिक गहन जांच प्रदान कर सकते हैं। उदाहरण के लिए, परीक्षण साधारण बग और गलतियाँ ढूंढने में प्रभावी है, लेकिन आम तौर पर इसे निष्पादित करना तेज़ और आसान होता है। औपचारिक सत्यापन, हालांकि उपयोग में अधिक बोझिल है, त्रुटियों की अनुपस्थिति को साबित करने या सूक्ष्म बग को प्रकट करने के लिए पर्याप्त शक्तिशाली है जो परीक्षण या कोड समीक्षाओं में छूटना आसान है।

विशिष्टता ओवरहेड

औपचारिक सत्यापन की मुख्य चुनौतियों में से एक औपचारिक विशिष्टताओं को लिखने और बनाए रखने का ओवरहेड है। इस प्रक्रिया में अक्सर एक विशेष भाषा का उपयोग करके विशिष्टताओं को मैन्युअल रूप से लिखने का समय लेने वाला कार्य शामिल होता है (जिसे कई डेवलपर्स को पहले सीखने की आवश्यकता होगी)। यह प्रक्रिया भी वृद्धिशील है, आम तौर पर सरल गुणों को लिखने और पहले उन्हें सत्यापित करने से शुरू होती है, फिर धीरे-धीरे शीर्ष पर अधिक जटिल गुणों को जोड़ती है। परीक्षण की तरह, यह एक ओपन-एंडेड प्रक्रिया है, जिसमें कोई स्पष्ट रोक बिंदु नहीं है, और कोई केवल उपलब्ध समय सीमा के भीतर जितनी संभव हो उतनी संपत्तियां जोड़ सकता है। इसके अतिरिक्त, जब डेवलपर्स सत्यापन के दौरान कोड बदलते हैं, तो उन्हें अपने मौजूदा विनिर्देशों को भी अपडेट करना होगा, जिससे अतिरिक्त रखरखाव प्रयास होंगे। ये कारक अतिरिक्त ओवरहेड करने में झिझकने वाले कुछ डेवलपर्स के लिए औपचारिक सत्यापन को एक कठिन काम बना सकते हैं।

और यद्यपि परीक्षण और औपचारिक सत्यापन एक साथ उपयोग किए जाने पर कोड की गुणवत्ता में सुधार कर सकते हैं, दोनों को विभिन्न भाषाओं और प्रारूपों में प्रोग्राम के अपेक्षित व्यवहार के विवरण (कभी-कभी समान) की आवश्यकता होती है। इन विवरणों को लिखना और बनाए रखना श्रम-गहन है, और एक ही विवरण के दो अलग-अलग रूपों को बनाए रखना दोहराए गए प्रयास जैसा महसूस हो सकता है। इससे निम्नलिखित प्रश्न उठता है: क्या अपेक्षित व्यवहार का वर्णन इस तरह से करना संभव है कि डेवलपर्स परीक्षण और सत्यापन दोनों के लिए उपयोग कर सकें?

प्रतीकात्मक परीक्षण और हेल्मोस के साथ परीक्षण और औपचारिक सत्यापन के बीच अंतर को पाटना

प्रतीकात्मक परीक्षण, प्रतीकात्मक इनपुट के साथ परीक्षण चलाने का अभ्यास, एक प्रभावी औपचारिक सत्यापन विधि है जो विनिर्देशन ओवरहेड को कम करता है। यह दृष्टिकोण परीक्षण और औपचारिक सत्यापन दोनों के लिए समान परीक्षण मामलों के उपयोग को सक्षम बनाता है। पारंपरिक परीक्षण के विपरीत, जो सत्यापित करता है कि एक प्रोग्राम इनपुट के सीमित सेट के लिए सही ढंग से काम करता है, प्रतीकात्मक परीक्षण सभी संभावित इनपुट के लिए प्रोग्राम की जांच करता है, इसलिए एक प्रोग्राम जो प्रतीकात्मक परीक्षण पास करता है उसे औपचारिक रूप से सत्यापित माना जा सकता है।

हेल्मोस एक औपचारिक सत्यापन उपकरण है जिसे प्रतीकात्मक परीक्षण के लिए डिज़ाइन किया गया है। अलग-अलग विशिष्टताओं की आवश्यकता या एक नई भाषा सीखने के बजाय, हेल्मोस मौजूदा परीक्षणों को औपचारिक विशिष्टताओं के रूप में उपयोग करता है। हेल्मोस के माध्यम से परीक्षण चलाने से स्वचालित रूप से सत्यापित हो जाएगा कि वे सभी संभावित इनपुट के लिए पास हैं, या प्रति-उदाहरण प्रदान करेंगे। यह न केवल अतिरिक्त विनिर्देश लेखन की आवश्यकता को समाप्त करता है, बल्कि औपचारिक सत्यापन उद्देश्यों के लिए यूनिट परीक्षण या फ़ज़िंग के लिए लिखे गए परीक्षणों के पुन: उपयोग की भी अनुमति देता है।

इस प्रकार डेवलपर्स के पास उनकी वर्तमान जरूरतों के आधार पर यूनिट परीक्षण, फ़ज़िंग और औपचारिक सत्यापन सहित गुणवत्ता आश्वासन विकल्पों की एक श्रृंखला से चुनने के लिए अधिक लचीलापन है। उदाहरण के लिए, परीक्षण सरल गलतियों की तुरंत पहचान कर सकते हैं, संभवतः फ़ज़र की मदद से जो यादृच्छिक इनपुट उत्पन्न करता है, और फिर हेल्मोस सभी इनपुटों में प्रोग्राम की शुद्धता में विश्वास को और बढ़ा सकता है।

उदाहरण: परीक्षण करना isPowerOfTwo() समारोह

उदाहरण के तौर पर निम्नलिखित पर विचार करें isPowerOfTwo() फ़ंक्शन, जो यह निर्धारित करता है कि दी गई संख्या दो की घात है या नहीं। यह फ़ंक्शन a का उपयोग करता है बिट हेरफेर एल्गोरिथ्म दक्षता के लिए, लेकिन इसकी शुद्धता साबित करना चुनौतीपूर्ण हो सकता है, खासकर उस मामले में जहां इनपुट दो की शक्ति नहीं है।

के लिए निम्नलिखित परीक्षण की कल्पना करें isPowerOfTwo() फ़ंक्शन: यह किसी दिए गए इनपुट के लिए अपेक्षित आउटपुट के साथ फ़ंक्शन के वास्तविक आउटपुट की तुलना करता है। यह एक पैरामीटरयुक्त परीक्षण है (जिसे संपत्ति-आधारित परीक्षण के रूप में भी जाना जाता है), जिसका अर्थ है कि आप इसे विभिन्न इनपुट मानों के साथ आसानी से चला सकते हैं, संभवतः फाउंड्री जैसे फ़ज़िंग टूल के साथ।

आप इस परीक्षण का उपयोग जांच करने के लिए कर सकते हैं isPowerOfTwo() यूनिट परीक्षण या फ़ज़ परीक्षण के माध्यम से कार्य करें, इसे इनपुट के चयन के साथ चलाएं। इस तरह के परीक्षण औपचारिक रूप से फ़ंक्शन की शुद्धता को साबित नहीं कर सकते हैं, क्योंकि हर संभावित इनपुट के लिए परीक्षण चलाना कम्प्यूटेशनल रूप से संभव नहीं है।

हालाँकि, हेल्मोस डेवलपर्स को थोड़े से अतिरिक्त प्रयास के साथ औपचारिक सत्यापन के लिए इन पूर्व-मौजूदा परीक्षणों का पुन: उपयोग करने की अनुमति देता है। उपकरण यह जाँचता है कि परीक्षण का प्रतीकात्मक निष्पादन करके परीक्षण सभी संभावित इनपुट के लिए पास हो गया है और फिर यह सत्यापित करता है कि दावे का कभी उल्लंघन नहीं हुआ है, (या, यदि दावा is उल्लंघन, एक प्रति-उदाहरण प्रदान करके)। इसका मतलब यह है कि यदि परीक्षण हेल्मोस से गुजरता है, तो फ़ंक्शन की शुद्धता को औपचारिक रूप से सत्यापित किया जाता है, जिसका अर्थ है कि एल्गोरिदम सही ढंग से कार्यान्वित किया गया है और कंपाइलर द्वारा बाइटकोड में सटीक रूप से अनुवाद किया गया है।

सीमा: सीमित प्रतीकात्मक निष्पादन

आम तौर पर पूरी तरह से स्वचालित, पूर्ण प्रतीकात्मक परीक्षण करना संभव नहीं है, क्योंकि इसके लिए समाधान की आवश्यकता होगी रुकने की समस्या, जो कि ज्ञात है अनिर्णनीय. इसका एक कारण यह है कि स्वचालित रूप से यह निर्धारित करना अक्सर असंभव होता है कि एक लूप को प्रतीकात्मक रूप से कितनी बार दोहराया जाना चाहिए। परिणामस्वरूप, पूरी तरह से स्वचालित औपचारिक सत्यापन आम तौर पर अनिर्णीत होता है।

इन मूलभूत सीमाओं को देखते हुए, हेल्मोस पूर्णता से अधिक स्वचालन को प्राथमिकता देता है। इस प्रयोजन के लिए, हेल्मोस को अनबाउंड लूप्स (जहां पुनरावृत्तियों की संख्या प्रोग्राम इनपुट पर निर्भर करती है) या चर-लंबाई सरणियों (स्ट्रिंग्स सहित) के लिए सीमित प्रतीकात्मक तर्क करने के लिए डिज़ाइन किया गया है। यह कुछ पूर्णता का त्याग करता है, लेकिन हेल्मोस को उपयोगकर्ता को लूप इनवेरिएंट जैसे अतिरिक्त एनोटेशन प्रदान करने की आवश्यकता से बचने की अनुमति देता है।

उदाहरण के लिए, के निम्नलिखित पुनरावृत्त संस्करण पर विचार करें isPowerOfTwo() फ़ंक्शन, जिसमें एक अनबाउंड लूप की सुविधा है, जहां लूप पुनरावृत्तियों की संख्या इनपुट संख्या का प्रतिनिधित्व करने के लिए आवश्यक बिट्स की न्यूनतम संख्या से निर्धारित होती है।

हेल्मोस प्रतीकात्मक रूप से इस असीमित लूप को केवल एक निर्दिष्ट सीमा तक पुनरावृत्त करता है। उदाहरण के लिए, यदि सीमा 3 पर सेट है, तो हेल्मोस लूप को अधिकतम 3 बार पुनरावृत्त करेगा और इनपुट मानों पर विचार नहीं करेगा जिसके कारण लूप 3 से अधिक बार पुनरावृत्त होगा (अर्थात, 2^3 से अधिक या उसके बराबर कोई भी मान ). इस विशेष मामले में, सीमा को 256 या उससे अधिक पर सेट करने से हेल्मोस पूरा हो सकेगा।

डेमो: हैल्मोस के साथ ERC721A का औपचारिक सत्यापन

हेल्मोस की क्षमताओं को प्रदर्शित करने के लिए, हमने इसका प्रतीकात्मक परीक्षण और औपचारिक सत्यापन किया ईआरसी721ए, ERC721 मानक का एक उच्च गैस-अनुकूलित कार्यान्वयन जो एकल ढलाई के लगभग समान लागत पर बैच ढलाई की अनुमति देता है। ERC721A में कई नवीन शामिल हैं अनुकूलन इस दक्षता को प्राप्त करने के लिए; उदाहरण के लिए, टोकन स्वामित्व डेटा को अपडेट करने में तब तक देरी करके गैस की बचत की जा सकती है जब तक कि टोकन हस्तांतरित नहीं हो जाता, ढलाई के समय नहीं। इसके लिए आलसी डेटा संरचना से स्वामित्व जानकारी को कुशलतापूर्वक पुनर्प्राप्त करने के लिए जटिल डेटा संरचनाओं और एल्गोरिदम के उपयोग की आवश्यकता होती है। और यद्यपि यह अनुकूलन गैस दक्षता में सुधार करता है, यह कोड जटिलता को भी बढ़ाता है और कार्यान्वयन की शुद्धता को साबित करना चुनौतीपूर्ण बनाता है। यह ERC721A को औपचारिक सत्यापन के लिए एक अच्छा उम्मीदवार बनाता है, क्योंकि यह कार्यान्वयन में विश्वास बढ़ा सकता है और संभावित उपयोगकर्ताओं को लाभान्वित कर सकता है।

प्रतीकात्मक परीक्षण गुण

चूँकि ERC721A के लिए मौजूदा परीक्षण जावास्क्रिप्ट में हार्डहैट (जो वर्तमान में हेल्मोस द्वारा समर्थित नहीं है) के साथ लिखे गए थे, हमने मुख्य प्रवेश बिंदु कार्यों के लिए सॉलिडिटी में नए परीक्षण लिखे: mint(), burn(), तथा transfer(). इन परीक्षणों ने जाँच की कि प्रत्येक फ़ंक्शन टोकन स्वामित्व और संतुलन को सही ढंग से अपडेट करता है, और अन्य उपयोगकर्ताओं के संतुलन या स्वामित्व में बदलाव किए बिना केवल प्रासंगिक उपयोगकर्ताओं को प्रभावित करता है। ERC721A में आलसी डेटा संरचना एल्गोरिदम के उपयोग के कारण बाद वाला साबित करना गैर-तुच्छ है। उदाहरण के लिए, निम्नलिखित परीक्षण जाँच करता है कि transfer() फ़ंक्शन निर्दिष्ट टोकन के स्वामित्व को सही ढंग से अपडेट करता है:

एक अन्य परीक्षण यह जाँचता है कि transfer() फ़ंक्शन अन्य पतों के लिए शेष राशि में परिवर्तन नहीं करता है, जिसे पहले बताए अनुसार साबित करना चुनौतीपूर्ण है:

सत्यापन परिणाम

हमने कुल मिलाकर ERC721A स्मार्ट अनुबंध पर हेल्मोस का उपयोग करके एक सत्यापन प्रयोग किया 19 परीक्षण. परीक्षण हेल्मोस के माध्यम से 3 के लूप अनरोलिंग बाउंड के साथ चलाए गए, जिसे पूरा होने में 16 मिनट लगे। सत्यापन समय का विवरण नीचे दी गई तालिका में देखा जा सकता है। यह प्रयोग मैकबुक प्रो पर एम1 प्रो चिप और 16 जीबी मेमोरी के साथ आयोजित किया गया था।

टेस्ट	समय
टेस्टबर्नबैलेंसअपडेट	6.67
testBurnNextTokenIdUnchanged	1.40
टेस्टबर्नअदरबैलेंसप्रिज़र्वेशन	5.69
testBurnअन्य स्वामित्व संरक्षण	189.70
टेस्टबर्नओनरशिपअपडेट	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintअन्य स्वामित्व संरक्षण	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceअपरिवर्तित	9.03
टेस्टट्रांसफरबैलेंसअपडेट	53.53
testTransferNextTokenIdUnchanged	4.47
टेस्टट्रांसफरअदरबैलेंसप्रिजर्वेशन	19.57
परीक्षणस्थानांतरणअन्यस्वामित्वसंरक्षण	430.61
टेस्टट्रांसफरओनरशिपअपडेट	18.71
परीक्षणस्थानांतरण आवश्यकताएँ	149.18

जबकि अधिकांश परीक्षण कुछ ही सेकंड में पूरे हो गए, उनमें से कुछ में कई मिनट लग गए। विचार किए जाने वाले मामलों की जटिल प्रकृति के कारण इन समय लेने वाली परीक्षणों को सत्यापित करना चुनौतीपूर्ण था, और आलसी डेटा संरचना एल्गोरिदम की शुद्धता से निकटता से संबंधित थे।

कुल मिलाकर, इस प्रयोग के नतीजे बताते हैं कि हेल्मोस स्मार्ट कॉन्ट्रैक्ट कोड की शुद्धता को प्रभावी ढंग से सत्यापित करने में सक्षम है। स्मार्ट अनुबंध की जटिलता और संभावित बढ़त के मामलों के बावजूद, यह कोड की अखंडता में बढ़ा हुआ विश्वास प्रदान करता है।

इंजेक्टेड बग के साथ प्रयोग करें

हेल्मोस के सीमित तर्क की प्रभावशीलता को प्रदर्शित करने के लिए, हमने इसका उपयोग ERC721A अनुबंध के पिछले संस्करण में बग का पता लगाने के लिए किया था। इस संस्करण में एक समस्या थी जिसने अंकगणितीय अतिप्रवाह को गलत तरीके से संभाला और संभावित रूप से बड़ी संख्या में टोकन को बैच-मिंट करने की अनुमति दी, जो आलसी डेटा संरचना की अखंडता को तोड़ सकता है और परिणामस्वरूप कुछ उपयोगकर्ताओं को अपना टोकन स्वामित्व खोना पड़ सकता है (एक समस्या) संकल्प वर्तमान संस्करण में)। हमने छोटी गाड़ी संस्करण पर ERC19A के लिए 721 परीक्षणों का एक ही सेट चलाया, और हैल्मोस इसके गुणों के लिए एक प्रति-उदाहरण ढूंढने में सक्षम था। mint() समारोह। विशेष रूप से, हेल्मोस ने इनपुट मान प्रदान किए जिसके कारण ऊपर वर्णित शोषण परिदृश्य सामने आया। इस प्रयोग के नतीजों से संकेत मिलता है कि, इसकी अपूर्णता के बावजूद, हेल्मोस का सीमित तर्क स्मार्ट अनुबंधों में शोषणकारी बगों का पता लगाने और उन्हें रोकने का एक प्रभावी तरीका हो सकता है।

संबंधित कार्य

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

जबकि हेल्मोस स्मार्ट अनुबंध सत्यापन के लिए उपलब्ध टूलसेट के लिए एक मूल्यवान अतिरिक्त है, इसका मतलब मौजूदा टूल को पूरक करना (प्रतिस्थापित नहीं करना) है। डेवलपर्स अपने अनुबंधों में उच्च स्तर का आश्वासन प्राप्त करने के लिए हेल्मोस को अन्य उपकरणों के साथ जोड़ सकते हैं। नीचे, हम हेल्मोस की तुलना कुछ चुनिंदा औपचारिक उपकरणों से करते हैं जो ईवीएम बाइटकोड का समर्थन करते हैं।

• K एक शक्तिशाली औपचारिक सत्यापन ढांचा है जो निगमनात्मक सत्यापन और इंटरैक्टिव प्रमेय सिद्ध करने में सक्षम बनाता है। इसका अंतर्निहित सिद्धांत और कार्यान्वयन उच्च स्तर की अभिव्यक्ति प्रदान करता है, जो इसे जटिल कार्यक्रमों और एल्गोरिदम को सत्यापित करने के लिए उपयुक्त बनाता है। हालाँकि, यह ध्यान दिया जाना चाहिए कि K को स्वचालित सत्यापन पर भारी जोर देने के साथ डिज़ाइन नहीं किया गया है और इसमें कुछ स्वचालन सुविधाओं का अभाव है जिसके लिए सत्यापन प्रक्रिया के दौरान अधिक मैन्युअल प्रयास की आवश्यकता हो सकती है। K फ्रेमवर्क का उपयोग करने के लिए, औपचारिक विनिर्देश K भाषा में लिखे जाते हैं, जिन्हें उपयोग से पहले सीखा जाना चाहिए। इसकी ताकत जटिल प्रणालियों को सत्यापित करने में विशेष रूप से उपयोगी है, जिसका स्वचालित तर्क का उपयोग करके विश्लेषण करना चुनौतीपूर्ण हो सकता है।
• प्रमाण पत्र स्मार्ट अनुबंधों के लिए एक औपचारिक सत्यापन उपकरण है जो स्वचालित सत्यापन पर केंद्रित है और हेल्मोस के समान बाउंडेड मॉडल चेकिंग का समर्थन करता है। सर्टोरा का उपयोग करने के लिए, डेवलपर्स को अपनी नई भाषा सीखनी होगी, CVL, विशिष्टताओं को लिखने के लिए। यह भाषा अनुबंध अपरिवर्तनीयों के माध्यम से कई महत्वपूर्ण गुणों के संक्षिप्त विवरण की अनुमति देती है, एक ऐसी सुविधा जिसका हेल्मोस वर्तमान में समर्थन नहीं करता है। एक बंद-स्रोत, मालिकाना उपकरण होने के बावजूद, सर्टोरा निरंतर विकास और अच्छे उपयोगकर्ता समर्थन के साथ मजबूत औपचारिक सत्यापन टूलिंग प्रदान करता है।
  
  दूसरी ओर, हल्मोस एक ओपन-सोर्स टूल है जो पैमाने में छोटा है और वर्तमान में सर्टोरा द्वारा प्रदान की गई कुछ सुविधाओं का अभाव है, लेकिन इसका उद्देश्य सार्वजनिक भलाई के रूप में सेवा करना है और इसका उद्देश्य बिना स्मार्ट अनुबंधों को शीघ्रता से सत्यापित करने के लिए एक विशिष्ट समाधान है। व्यापक सेटअप और रखरखाव की आवश्यकता.
• एचईवीएम एक अन्य औपचारिक सत्यापन उपकरण है जो हेल्मोस के समान है। यह पहले DappTools का हिस्सा था, जो फाउंड्री का अग्रदूत है। एचईवीएम और हेल्मोस दोनों में एक अलग विनिर्देश की आवश्यकता नहीं होने की सुविधा है और दावे के उल्लंघन की पहचान करने के लिए प्रतीकात्मक रूप से मौजूदा परीक्षणों को निष्पादित कर सकते हैं। यह उपयोगकर्ताओं को दोनों उपकरणों का परस्पर उपयोग करने या उन्हें एक ही परीक्षण के लिए समानांतर में चलाने की अनुमति देता है, जिससे उन्हें प्रतीकात्मक परीक्षण के लिए कई विकल्प मिलते हैं।
  
  यह ध्यान देने योग्य है कि, उनकी समानताओं के बावजूद, HEVM और हेल्मोस को स्वतंत्र रूप से विकसित किया गया है और उनके कार्यान्वयन विवरण में भिन्नता है; विशेष रूप से अनुकूलन और प्रतीकात्मक तर्क रणनीतियों के संदर्भ में। इसके अतिरिक्त, HEVM को हास्केल में लिखा गया है, जबकि हेल्मोस को पायथन में लिखा गया है, जो समृद्ध पायथन पारिस्थितिकी तंत्र को उजागर करता है। दोनों टूल का उपयोग करने की क्षमता होने से उपयोगकर्ताओं को स्मार्ट अनुबंधों की सुरक्षा और शुद्धता सुनिश्चित करने के लिए अधिक लचीलापन और विकल्प मिलते हैं।

हेल्मोस खुला स्रोत है, और वर्तमान में अपने बीटा चरण में है। हम नए पर सक्रिय रूप से काम कर रहे हैं विशेषताएं और कार्यक्षमता, जिसमें फाउंड्री चीट कोड और कई अन्य प्रमुख प्रयोज्य विशेषताएं शामिल हैं। हम आपके विचारों की बहुत सराहना करेंगे कि कौन सी सुविधाएँ सबसे महत्वपूर्ण हैं, और हेल्मोस को सभी के लिए एक बेहतर उपकरण बनाने के लिए किसी भी प्रतिक्रिया, सुझाव और योगदान का स्वागत करते हैं।

**

यहां व्यक्त किए गए विचार व्यक्तिगत एएच कैपिटल मैनेजमेंट, एलएलसी ("a16z") कर्मियों के हैं जिन्हें उद्धृत किया गया है और यह a16z या इसके सहयोगियों के विचार नहीं हैं। यहां निहित कुछ जानकारी तृतीय-पक्ष स्रोतों से प्राप्त की गई है, जिसमें a16z द्वारा प्रबंधित निधियों की पोर्टफोलियो कंपनियों से भी शामिल है। विश्वसनीय माने जाने वाले स्रोतों से लिए गए, a16z ने स्वतंत्र रूप से ऐसी जानकारी का सत्यापन नहीं किया है और किसी भी स्थिति के लिए जानकारी की वर्तमान या स्थायी सटीकता या इसकी उपयुक्तता के बारे में कोई प्रतिनिधित्व नहीं करता है। इसके अतिरिक्त, इस सामग्री में तृतीय-पक्ष विज्ञापन शामिल हो सकते हैं; a16z ने ऐसे विज्ञापनों की समीक्षा नहीं की है और उनमें निहित किसी भी विज्ञापन सामग्री का समर्थन नहीं करता है।

यह सामग्री केवल सूचना के उद्देश्यों के लिए प्रदान की जाती है, और कानूनी, व्यापार, निवेश या कर सलाह के रूप में इस पर भरोसा नहीं किया जाना चाहिए। आपको उन मामलों में अपने स्वयं के सलाहकारों से परामर्श लेना चाहिए। किसी भी प्रतिभूति या डिजिटल संपत्ति के संदर्भ केवल दृष्टांत उद्देश्यों के लिए हैं, और निवेश सलाहकार सेवाएं प्रदान करने के लिए एक निवेश अनुशंसा या प्रस्ताव का गठन नहीं करते हैं। इसके अलावा, यह सामग्री किसी भी निवेशक या संभावित निवेशकों द्वारा उपयोग के लिए निर्देशित नहीं है और न ही इसका इरादा है, और किसी भी परिस्थिति में a16z द्वारा प्रबंधित किसी भी फंड में निवेश करने का निर्णय लेते समय इस पर भरोसा नहीं किया जा सकता है। (a16z फंड में निवेश करने की पेशकश केवल निजी प्लेसमेंट मेमोरेंडम, सब्सक्रिप्शन एग्रीमेंट, और ऐसे किसी भी फंड के अन्य प्रासंगिक दस्तावेज द्वारा की जाएगी और इसे पूरी तरह से पढ़ा जाना चाहिए।) किसी भी निवेश या पोर्टफोलियो कंपनियों का उल्लेख, संदर्भित, या वर्णित a16z द्वारा प्रबंधित वाहनों में सभी निवेशों के प्रतिनिधि नहीं हैं, और इस बात का कोई आश्वासन नहीं दिया जा सकता है कि निवेश लाभदायक होगा या भविष्य में किए गए अन्य निवेशों में समान विशेषताएं या परिणाम होंगे। आंद्रेसेन होरोविट्ज़ द्वारा प्रबंधित निधियों द्वारा किए गए निवेशों की सूची (उन निवेशों को छोड़कर जिनके लिए जारीकर्ता ने सार्वजनिक रूप से कारोबार की गई डिजिटल संपत्ति में सार्वजनिक रूप से और साथ ही अघोषित निवेशों का खुलासा करने के लिए a16z की अनुमति नहीं दी है) https://a16z.com/investments पर उपलब्ध है। /.

इसमें दिए गए चार्ट और ग्राफ़ केवल सूचना के उद्देश्यों के लिए हैं और निवेश का कोई भी निर्णय लेते समय उन पर भरोसा नहीं किया जाना चाहिए। पूर्व प्रदर्शन भविष्य के परिणाम का संकेत नहीं है। सामग्री केवल इंगित तिथि के अनुसार बोलती है। इन सामग्रियों में व्यक्त किए गए किसी भी अनुमान, अनुमान, पूर्वानुमान, लक्ष्य, संभावनाएं और/या राय बिना किसी सूचना के परिवर्तन के अधीन हैं और दूसरों द्वारा व्यक्त की गई राय के विपरीत या भिन्न हो सकते हैं। अतिरिक्त महत्वपूर्ण जानकारी के लिए कृपया https://a16z.com/disclosures देखें।