इस प्रोजेक्ट के बारे में

Kani Rust प्रोग्रामों के लिए एक बिट-सटीक मॉडल चेकर है, जिसे model-checking संगठन के अंतर्गत विकसित किया गया है। इसे डेवलपर्स को Rust कोड की सुरक्षा और शुद्धता दोनों की जाँच करने में मदद करने के लिए डिज़ाइन किया गया है। सुरक्षा पक्ष पर, Kani कई प्रकार के अपरिभाषित व्यवहार की स्वचालित रूप से जाँच करता है। यह Rust में unsafe कोड ब्लॉक को सत्यापित करने के लिए विशेष रूप से मूल्यवान है, जहाँ कंपाइलर सामान्य सुरक्षा गारंटी लागू नहीं करता है। शुद्धता पक्ष पर, यह स्वचालित रूप से पैनिक (जैसे None पर unwrap() कॉल करना), अंकगणितीय ओवरफ्लो, और कस्टम शुद्धता गुणों की जाँच करता है जिन्हें एसर्शन (assert!(...)) या फ़ंक्शन अनुबंधों के रूप में व्यक्त किया जाता है। उपयोग परीक्षण-जैसी कार्यप्रणाली का अनुसरण करता है। डेवलपर्स #[kani::proof] से एनोटेटेड एक हार्नेस लिखते हैं और गैर-नियतात्मक इनपुट बनाने के लिए kani::any() का उपयोग करते हैं। फिर Kani यह सिद्ध करने का प्रयास करता है कि सभी मान्य इनपुट बिना पैनिक या अप्रत्याशित व्यवहार के, विनिर्देश को संतुष्ट करने वाले आउटपुट उत्पन्न करते हैं। Kani बुक में एक ट्यूटोरियल और संदर्भ दस्तावेज़ उपलब्ध हैं। इंस्टॉलेशन 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 दोनों लाइसेंसों के अंतर्गत वितरित किया जाता है, और इसमें Rust प्रोजेक्ट का कोड शामिल है। इसका एक अकादमिक उद्धरण (ASE 2026 पेपर) है और योगदानकर्ताओं के लिए डेवलपर दस्तावेज़ प्रदान करता है।