మేము Runtime Verification, క్లిష్టమైన సిస్టమ్ల భద్రత మరియు ఖచ్చితత్వాన్ని నిర్ధారించడానికి కఠినమైన సాధనాలను నిర్మిస్తున్న పరిశోధన మరియు అభివృద్ధి సంస్థ. మా బృందం K Frameworkలో వ్రాయబడిన Ethereum Virtual Machine (EVM) యొక్క అత్యంత పూర్తి మరియు బ్యాటిల్-టెస్టెడ్ ఫార్మల్ సెమాంటిక్స్ అయిన KEVMను అభివృద్ధి చేసింది. KEVM కేవలం ఒక స్పెసిఫికేషన్ మాత్రమే కాదు, ఇది స్మార్ట్ కాంట్రాక్ట్ల గురించి సింబాలిక్గా తార్కికం చేయడానికి, కన్ఫార్మెన్స్ టెస్ట్లను రన్ చేయడానికి, గ్యాస్ వినియోగాన్ని విశ్లేషించడానికి, ప్రోగ్రామ్లను డీబగ్ చేయడానికి మరియు కరెక్ట్నెస్ ప్రాపర్టీలను ఫార్మల్గా ధృవీకరించడానికి ఉపయోగించగల ఎగ్జిక్యూటబుల్ స్పెసిఫికేషన్. ఇది పూర్తి Ethereum టెస్ట్ సూట్ను పాస్ చేస్తుంది మరియు Solidity మరియు Vyper రెండింటిలోనూ ERC20 టోకెన్లతో సహా అధిక-విలువ కాంట్రాక్ట్లను ధృవీకరించడానికి ఉపయోగించబడుతుంది. Pectra అప్గ్రేడ్కు మద్దతు ఇవ్వడానికి మేము ఇటీవల సెమాంటిక్స్ను అప్డేట్ చేసాము. KEVMను Kontrol చురుకుగా ఉపయోగిస్తోంది - ఇది Soldiity కోసం మా ఫార్మల్ వెరిఫికేషన్ టూల్, దీనిని Optimism, Ethereum Foundation, Lido, Uniswapతో సహా EVM పర్యావరణ వ్యవస్థలోని ప్రముఖ బృందాలు, అలాగే విస్తృత Ethereum కమ్యూనిటీ అంతటా ఉన్న భద్రతా పరిశోధకులు మరియు ఆడిటర్లు చురుకుగా ఉపయోగిస్తున్నారు. మేము ఈ రిపోజిటరీని చురుకుగా నిర్వహిస్తాము, Ethereum యొక్క ప్రోటోకాల్ పరిణామానికి సహకరిస్తాము మరియు Foundry వంటి డెవలపర్ టూలింగ్తో ఇంటిగ్రేట్ చేస్తాము. KEVM ద్వారా, నిరూపించదగిన సరైన మరియు సురక్షితమైన స్మార్ట్ కాంట్రాక్ట్ ఇన్ఫ్రాస్ట్రక్చర్లో సాధ్యమయ్యే వాటి సరిహద్దులను మేము విస్తరిస్తున్నాము.
