নিরাপত্তা ও টেস্টিং

Certora AutoProver

বিধিবদ্ধ যাচাইকরণ

বিধিবদ্ধ যাচাইকরণ · যাচাইকরণ

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

সম্পর্কিত রিসোর্স

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

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

Kontrol - formal verification tool based on Foundry and KEVM

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

Act

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

Verifereum

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

Certora Prover

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.