ప్రధాన కంటెంట్‌కు దాటవేయండి
భద్రత & టెస్టింగ్

Certora Prover

నియత ధృవీకరణ

GitHub లో చూడండి (కొత్త ట్యాబ్‌లో తెరవబడుతుంది)

తర్వాతది చూడండి

Kontrol - formal verification tool based on Foundry and KEVM

Certora Prover గురించి

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.

ట్యాగ్‌లు

  • నియత ధృవీకరణ
  • ధృవీకరణ
  • భద్రత

రిపోజిటరీCertora

సమాచారం

రకం
నియత ధృవీకరణ
GitHub స్టార్స్
339
లైసెన్స్
GPL-3.0
జాబితా సమీక్షించబడింది
సెప్టెంబర్ 2026

సారూప్య సాధనాలు

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

hax

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

Act

Act

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