सुरक्षा आणि चाचणी

Verifereum

औपचारिक पडताळणी

वेबसाइटला भेट द्या

पुढे पहा

Certora AutoProver

Verifereum बद्दल

Verifereum इथेरियम स्मार्ट कॉन्ट्रॅक्ट्सना HOL4-समर्थित थिअरम प्रूव्हिंगशी जोडते, जेणेकरून जेव्हा स्वयंचलित SMT दृष्टिकोन पुरेसे नसतात तेव्हा तुम्ही अत्यंत भक्कम अचूकतेचे दावे साध्य करू शकता.

टॅग्स

सुरक्षा
शिक्षण
औपचारिक पडताळणी

रिपॉझिटरीverifereum

verifereum54 (नवीन टॅबमध्ये उघडते)

माहिती

प्रकार: औपचारिक पडताळणी
GitHub स्टार्स: 54
परवाना: GPL-3.0
लिस्टिंगचे पुनरावलोकन केले: जून 2026

समान टूल्स

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM हे EVM चे K-framework एक्झिक्युटेबल सिमेंटिक्स आहे: जेव्हा तुम्हाला कन्फॉर्मन्स-चेक्ड एक्झिक्युशन, सिम्बॉलिक एक्सप्लोरेशन, गॅस रिझनिंग, किंवा इथेरियमच्या नियमांचा बारकाईने मागोवा घेणाऱ्या पुराव्यांची आवश्यकता असते, तेव्हा त्याला बाइटकोडवर निर्देशित करा.

hax

hax हे Rust च्या मोठ्या उपसंचाचे F* किंवा Rocq सारख्या फॉर्मल लँग्वेजेसमध्ये हाय ॲश्युरन्स ट्रान्सलेशन्स करण्यासाठी एक टूल आहे.

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.