kani

Kani est un vérificateur de modèles bit-précis pour les programmes Rust, développé sous l'organisation model-checking. Il est conçu pour aider les développeurs à vérifier à la fois la sécurité et la correction du code Rust. Côté sécurité, Kani vérifie automatiquement de nombreux types de comportements indéfinis. Cela le rend particulièrement précieux pour vérifier les blocs de code unsafe en Rust, où le compilateur n'applique pas les garanties de sécurité habituelles. Côté correction, il vérifie automatiquement les paniques (comme appeler unwrap() sur None), les débordements arithmétiques et les propriétés de correction personnalisées exprimées soit comme des assertions (assert!(...)) soit comme des contrats de fonction. L'utilisation suit un flux de travail similaire aux tests. Les développeurs écrivent un harnais annoté avec #[kani::proof] et utilisent kani::any() pour créer des entrées non déterministes. Kani tente ensuite de prouver que toutes les entrées valides produisent des sorties satisfaisant la spécification, sans paniquer ni présenter de comportement inattendu. Un tutoriel et une documentation de référence sont disponibles dans le livre Kani. L'installation se fait via Cargo : cargo install --locked kani-verifier suivi de cargo kani setup. L'outil prend en charge Rust 1.58+ sur Linux ou macOS. Une action GitHub (model-checking/kani-github-action) permet l'intégration dans les pipelines CI. Le projet est distribué sous les licences MIT et Apache 2.0, et il contient du code du projet Rust. Il a une citation académique (article ASE 2026) et fournit une documentation pour les développeurs contributeurs.