Runtime Verification एक दशक से अधिक समय से ओपन-सोर्स औपचारिक सत्यापन टूल में सबसे आगे रहा है। हमारा सामान्य दृष्टिकोण हमें कई ब्लॉकचेन पर अपनी तकनीक का उपयोग करने की अनुमति देता है। जबकि KEVM सभी EVM-आधारित स्मार्ट कॉन्ट्रैक्ट को हमारा सत्यापन इंफ्रास्ट्रक्चर प्रदान करता है, Kontrol Solidity स्मार्ट कॉन्ट्रैक्ट के लिए औपचारिक सत्यापन में प्रवेश की बाधा को काफी कम कर देता है। हमारी टूलिंग पूरी तरह से ओपन सोर्स है और बिना किसी अतिरिक्त लागत के Optimism इकोसिस्टम के सभी डेवलपर्स के लिए स्वतंत्र रूप से सुलभ है। KEVM K फ्रेमवर्क में लिखा गया एक EVM निष्पादन योग्य औपचारिक सिमेंटिक्स है। KEVM सभी Ethereum अनुरूपता परीक्षण पास करता है और K फ्रेमवर्क के साथ स्मार्ट कॉन्ट्रैक्ट को औपचारिक रूप से सत्यापित करने के लिए प्रवेश बिंदु है। हालांकि, सादे KEVM का उपयोग करने के लिए विनिर्देश लिखने के लिए K फ्रेमवर्क पर तदर्थ प्रशिक्षण की आवश्यकता होती है। इसके अतिरिक्त, ये विनिर्देश काफी विस्तृत हो सकते हैं, जिससे उन्हें लिखने की कठिनाई बढ़ जाती है। Kontrol डेवलपर्स को अपने स्मार्ट कॉन्ट्रैक्ट के औपचारिक विनिर्देश को सीधे Foundry प्रॉपर्टी टेस्ट के रूप में लिखने की अनुमति देकर इसे हल करता है। इन परीक्षणों को स्वचालित रूप से KEVM विनिर्देशों में अनुवादित किया जाता है, जो बहुत आसान डेवलपर अनुभव की अनुमति देते हुए सभी सत्यापन गारंटी को बनाए रखता है।
