Verifereum

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.