Verifereum

KEVM হলো EVM-এর K-framework এক্সিকিউটেবল সিম্যান্টিকস: যখন আপনার কনফরম্যান্স-চেকড এক্সিকিউশন, সিম্বলিক এক্সপ্লোরেশন, গ্যাস রিজনিং, বা ইথেরিয়ামের নিয়মগুলো ঘনিষ্ঠভাবে অনুসরণ করে এমন প্রমাণের প্রয়োজন হয়, তখন এটিকে বাইটকোডে পয়েন্ট করুন।

Kontrol Foundry-এর প্রপার্টি টেস্টগুলোকে KEVM-সমর্থিত প্রমাণে উন্নীত করে, যাতে আপনি শুধুমাত্র সাধারণ KEVM-এর তুলনায় অনেক কম হাতে-লেখা স্পেসিফিকেশনের কাজ করে বিধিবদ্ধ নিশ্চয়তা অর্জন করতে পারেন।

hax হলো Rust-এর একটি বড় সাবসেটকে F* বা Rocq-এর মতো ফরমাল ল্যাঙ্গুয়েজে হাই অ্যাসিওরেন্স ট্রান্সলেশনের জন্য একটি টুল।

Act হলো ইথেরিয়ামের ডিক্লারেটিভ স্পেসিফিকেশন ভাষা এবং টুলচেইন যা একটি EVM প্রোগ্রামের সমস্ত আচরণ বর্ণনা করার জন্য ব্যবহৃত হয়, যাতে SMT সলভার, থিওরেম প্রুভার, বা অর্থনৈতিক বিশ্লেষণ টুলগুলো বাইটকোড-স্তরের সঠিকতা এবং ইনসেনটিভ সামঞ্জস্যতা সম্পর্কে যৌক্তিক বিশ্লেষণ করতে পারে, যার মধ্যে কংক্রিট ইমপ্লিমেন্টেশনের বিপরীতে স্বয়ংক্রিয় রিফাইনমেন্ট প্রুফ অন্তর্ভুক্ত রয়েছে।