आम्ही Runtime Verification आहोत, एक रिसर्च आणि डेव्हलपमेंट कंपनी जी क्रिटिकल सिस्टीम्सची सुरक्षितता आणि अचूकता सुनिश्चित करण्यासाठी कठोर टूल्स तयार करते. आमच्या टीमने KEVM विकसित केले आहे, जे K Framework मध्ये लिहिलेले Ethereum Virtual Machine (EVM) चे सर्वात परिपूर्ण आणि बॅटल-टेस्टेड फॉर्मल सिमेंटिक्स आहे. KEVM हे केवळ एक स्पेसिफिकेशन नाही, तर ते एक एक्झिक्यूटेबल स्पेसिफिकेशन आहे ज्याचा वापर स्मार्ट कॉन्ट्रॅक्ट्सबद्दल सिम्बॉलिकली विचार करण्यासाठी, कन्फॉर्मन्स टेस्ट्स चालवण्यासाठी, गॅस वापराचे विश्लेषण करण्यासाठी, प्रोग्राम्स डीबग करण्यासाठी आणि करेक्टनेस प्रॉपर्टीज फॉर्मली व्हेरिफाय करण्यासाठी केला जाऊ शकतो. हे संपूर्ण Ethereum टेस्ट सूट पास करते आणि Solidity आणि Vyper दोन्हीमधील ERC-20 टोकन्ससह हाय-व्हॅल्यू कॉन्ट्रॅक्ट्स व्हेरिफाय करण्यासाठी वापरले जाते. आम्ही अलीकडेच Pectra अपग्रेडला सपोर्ट करण्यासाठी सिमेंटिक्स अपडेट केले आहेत. KEVM चा सक्रियपणे Kontrol द्वारे वापर केला जात आहे - आमचे Soldiity साठी फॉर्मल व्हेरिफिकेशन टूल, जे Optimism, Ethereum Foundation, Lido, Uniswap यांसारख्या EVM इकोसिस्टीममधील आघाडीच्या टीम्स तसेच व्यापक Ethereum कम्युनिटीमधील सिक्युरिटी रिसर्चर्स आणि ऑडिटर्सद्वारे सक्रियपणे वापरले जाते. आम्ही ही रिपॉझिटरी सक्रियपणे मेंटेन करतो, Ethereum च्या प्रोटोकॉल इव्होल्यूशनमध्ये योगदान देतो आणि Foundry सारख्या डेव्हलपर टूलिंगसोबत इंटिग्रेट करतो. KEVM द्वारे, आम्ही प्रूव्हेबली करेक्ट आणि सुरक्षित स्मार्ट कॉन्ट्रॅक्ट इन्फ्रास्ट्रक्चरमध्ये काय शक्य आहे याच्या सीमा विस्तारत आहोत.
