প্রকল্প সম্পর্কে

কানি হলো রাস্ট প্রোগ্রামের জন্য একটি বিট-নির্ভুল মডেল চেকার, যা মডেল-চেকিং সংস্থার অধীনে তৈরি। এটি ডেভেলপারদের রাস্ট কোডের নিরাপত্তা এবং সঠিকতা উভয়ই পরীক্ষা করতে সহায়তা করার জন্য ডিজাইন করা হয়েছে। নিরাপত্তার দিক থেকে, কানি স্বয়ংক্রিয়ভাবে অনেক ধরনের অনির্ধারিত আচরণ পরীক্ষা করে। এটি রাস্টের অনিরাপদ কোড ব্লক যাচাই করার জন্য বিশেষভাবে মূল্যবান, যেখানে কম্পাইলার স্বাভাবিক নিরাপত্তা গ্যারান্টি প্রয়োগ করে না। সঠিকতার দিক থেকে, এটি স্বয়ংক্রিয়ভাবে প্যানিক (যেমন None-এ unwrap() কল করা), অ্যারিথমেটিক ওভারফ্লো এবং কাস্টম সঠিকতা বৈশিষ্ট্য পরীক্ষা করে, যা অ্যাসারশন (assert!(...)) বা ফাংশন কন্ট্রাক্ট হিসেবে প্রকাশ করা হয়। ব্যবহার একটি টেস্টিং-সদৃশ কর্মপ্রবাহ অনুসরণ করে। ডেভেলাররা #[kani::proof] দিয়ে চিহ্নিত একটি হারনেস লেখেন এবং kani::any() ব্যবহার করে নন-ডিটারমিনিস্টিক ইনপুট তৈরি করেন। কানি তখন প্রমাণ করার চেষ্টা করে যে সমস্ত বৈধ ইনপুট স্পেসিফিকেশন পূরণ করে এমন আউটপুট তৈরি করে, প্যানিক বা অপ্রত্যাশিত আচরণ ছাড়াই। কানি বইয়ে একটি টিউটোরিয়াল এবং রেফারেন্স ডকুমেন্টেশন উপলব্ধ। ইনস্টলেশন Cargo-এর মাধ্যমে করা হয়: cargo install --locked kani-verifier এবং তারপর cargo kani setup। টুলটি Linux বা macOS-এ Rust 1.58+ সমর্থন করে। একটি GitHub Action (model-checking/kani-github-action) CI পাইপলাইনে সংহত করার অনুমতি দেয়। প্রকল্পটি MIT এবং Apache 2.0 উভয় লাইসেন্সের অধীনে বিতরণ করা হয়, এবং এতে রাস্ট প্রকল্পের কোড রয়েছে। এটির একটি একাডেমিক উদ্ধৃতি (ASE 2026 পেপার) রয়েছে এবং অবদানকারীদের জন্য ডেভেলপার ডকুমেন্টেশন প্রদান করে।