Act

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

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.