K Semantics of the Ethereum Virtual Machine (EVM)

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.

Kontrol, Foundry प्रॉपर्टी टेस्ट को KEVM-समर्थित प्रमाणों में बदल देता है, जिससे आप अकेले रॉ KEVM की तुलना में कम हस्तलिखित विनिर्देश कार्य के साथ औपचारिक गारंटी प्राप्त कर सकते हैं।

Act इथेरियम की एक घोषणात्मक विनिर्देश भाषा और टूलचेन है, जो किसी EVM प्रोग्राम के सभी व्यवहारों का वर्णन करती है ताकि SMT सॉल्वर, थ्योरम प्रूवर, या आर्थिक विश्लेषण उपकरण बाइटकोड-स्तर की शुद्धता और प्रोत्साहन संगतता के बारे में तर्क कर सकें, जिसमें ठोस कार्यान्वयन के विरुद्ध स्वचालित शोधन प्रमाण शामिल हैं।