मुख्य सामग्रीवर जा
सुरक्षा आणि चाचणी

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

hax

hax

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

Act

Act

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