منصوبے کے بارے میں

Kani Rust پروگراموں کے لیے ایک bit-precise model checker ہے، جسے model-checking organization کے تحت تیار کیا گیا ہے۔ اسے ڈویلپرز کو Rust code کی حفاظت اور درستگی دونوں کی جانچ میں مدد کے لیے ڈیزائن کیا گیا ہے۔ حفاظت کے لحاظ سے، Kani خود بخود کئی قسم کے undefined behavior کی جانچ کرتا ہے۔ اسے Rust میں unsafe code blocks کی تصدیق کے لیے خاص طور پر قیمتی بناتا ہے، جہاں compiler عمومی حفاظتی ضمانتوں کو نافذ نہیں کرتا۔ درستگی کے لحاظ سے، یہ خود بخود panics (جیسے None پر unwrap() کو کال کرنا)، arithmetic overflows، اور custom correctness properties کی جانچ کرتا ہے جو یا تو assertions (assert!(...)) یا function contracts کے طور پر ظاہر ہوتے ہیں۔ استعمال ایک testing جیسے workflow کی پیروی کرتا ہے۔ ڈویلپرز #[kani::proof] کے ساتھ annotated harness لکھتے ہیں اور nondeterministic inputs بنانے کے لیے kani::any() استعمال کرتے ہیں۔ پھر Kani یہ ثابت کرنے کی کوشش کرتا ہے کہ تمام valid inputs specification کو پورا کرنے والے outputs پیدا کرتے ہیں، بغیر panicking یا غیر متوقع behavior کے۔ Kani book میں ایک tutorial اور reference documentation دستیاب ہے۔ تنصیب Cargo کے ذریعے کی جاتی ہے: cargo install --locked kani-verifier کے بعد cargo kani setup۔ یہ ٹول Linux یا macOS پر Rust 1.58+ کو سپورٹ کرتا ہے۔ ایک GitHub Action (model-checking/kani-github-action) CI pipelines میں انضمام کی سہولت دیتا ہے۔ یہ پروجیکٹ MIT اور Apache 2.0 دونوں لائسنسز کے تحت تقسیم کیا جاتا ہے، اور اس میں Rust پروجیکٹ کا code شامل ہے۔ اس کی ایک academic citation (ASE 2026 paper) ہے اور یہ contributors کے لیے developer documentation فراہم کرتا ہے۔