hax

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

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

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

Verifereum ইথেরিয়াম স্মার্ট কন্ট্রাক্টগুলোকে HOL4-ব্যাকড থিওরেম প্রুভিংয়ের সাথে যুক্ত করে, যাতে স্বয়ংক্রিয় SMT পদ্ধতিগুলো যথেষ্ট না হলে আপনি অত্যন্ত শক্তিশালী সঠিকতার দাবি করার লক্ষ্য রাখতে পারেন।