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