Security & testing

Act

Formal verification

విద్య · అనలిటిక్స్ · నియత ధృవీకరణ · సింబాలిక్ ఎగ్జిక్యూషన్

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

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

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

hax

hax అనేది Rust యొక్క పెద్ద ఉపసమితిని F* లేదా Rocq వంటి ఫార్మల్ లాంగ్వేజ్‌లలోకి హై అస్యూరెన్స్ అనువాదాల కోసం ఒక టూల్.

Verifereum

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