Key points are not available for this paper at this time.
स्मार्ट अनुबंध वे प्रोग्राम हैं जिन्हें ब्लॉकचेन नेटवर्क द्वारा अविश्वसनीय उपयोगकर्ताओं के बीच क्रिप्टो-एसेट के अदला-बदली को नियंत्रित करने के लिए निष्पादित किया जाता है। उनकी अपरिवर्तनीयता, सार्वजनिक पहुंच और उच्च दांव के कारण, स्मार्ट अनुबंध हमलावरों के लिए एक आकर्षक लक्ष्य हैं, जैसा कि सुरक्षा घटनाओं के लंबे इतिहास ने साबित किया है। यह एथेरियम, प्रमुख स्मार्ट अनुबंध प्लेटफ़ॉर्म, और सॉलिडिटी, इसकी मुख्य स्मार्ट अनुबंध भाषा पर औपचारिक तरीकों के अनुप्रयोग के लिए एक प्रेरक कारक रहा है, जो विभिन्न उद्देश्यों के साथ पुष्टि उपकरणों का लक्ष्य बन गए हैं। इन उपकरणों की एक वर्तमान सीमा यह है कि वे वास्तव में क्रिप्टो-एसेट के अदला-बदली के संबंध में तरलता गुणों को व्यक्त करने और सत्यापित करने में प्रभावी नहीं हैं: उदाहरण के लिए, क्या यह सच है कि प्रत्येक पहुंच योग्य स्थिति में एक उपयोगकर्ता एक निर्दिष्ट मात्रा में क्रिप्टो-एसेट को निकालने के लिए लेनदेन की एक श्रृंखला शुरू कर सकता है? हम सॉल्वेंट का प्रस्ताव करते हैं, जो इन प्रकार के गुणों को सत्यापित करने के लिए एक उपकरण है, जो सॉलिडिटी के लिए मौजूदा सत्यापन उपकरणों की पहुंच से परे हैं। हम स्मार्ट अनुबंधों के एक सामान्य बेंचमार्क के माध्यम से सॉल्वेंट की प्रभावशीलता और प्रदर्शन का मूल्यांकन करते हैं।
बार्टोलेटी और अन्य (सप्त,) ने इस प्रश्न का अध्ययन किया।