hax

KEVM అనేది EVM యొక్క K-ఫ్రేమ్‌వర్క్ ఎక్జిక్యూటబుల్ సెమాంటిక్స్: మీకు కన్ఫార్మెన్స్-చెక్ చేయబడిన ఎక్జిక్యూషన్, సింబాలిక్ ఎక్స్‌ప్లోరేషన్, గ్యాస్ రీజనింగ్ లేదా ఎథీరియం నియమాలను దగ్గరగా ట్రాక్ చేసే నిరూపణలు అవసరమైనప్పుడు దీనిని బైట్‌కోడ్‌కు పాయింట్ చేయండి.

Kontrol, Foundry ప్రాపర్టీ పరీక్షలను KEVM-ఆధారిత నిరూపణలుగా మారుస్తుంది, తద్వారా మీరు కేవలం ముడి KEVM కంటే తక్కువ చేతితో వ్రాసిన స్పెసిఫికేషన్ పనితో నియత హామీలను సాధించవచ్చు.

Act అనేది EVM ప్రోగ్రామ్ యొక్క అన్ని ప్రవర్తనలను వివరించడానికి ఉపయోగించే ఎథీరియం యొక్క డిక్లరేటివ్ స్పెసిఫికేషన్ లాంగ్వేజ్ మరియు టూల్‌చైన్, తద్వారా SMT సాల్వర్‌లు, థీరమ్ ప్రూవర్‌లు లేదా ఆర్థిక విశ్లేషణ సాధనాలు కాంక్రీట్ ఇంప్లిమెంటేషన్‌లకు వ్యతిరేకంగా ఆటోమేటిక్ రిఫైన్‌మెంట్ ప్రూఫ్‌లతో సహా బైట్‌కోడ్-స్థాయి ఖచ్చితత్వం మరియు ప్రోత్సాహక అనుకూలత గురించి తార్కికంగా విశ్లేషించగలవు.

స్వయంచాలక SMT విధానాలు సరిపోనప్పుడు మీరు చాలా బలమైన ఖచ్చితత్వ వాదనలను లక్ష్యంగా చేసుకోవడానికి వీలుగా, Verifereum ఎథీరియం స్మార్ట్ కాంట్రాక్ట్‌లను HOL4-ఆధారిత సిద్ధాంత నిరూపణకు అనుసంధానిస్తుంది.