Verifereum

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

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

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.