Verus : un analyseur statique pour vérifier l'exactitude du code Rust

Verus est un outil d'analyse statique pour vérifier l'exactitude du code écrit en Rust. Les développeurs écrivent des spécifications de ce que leur code doit faire, et Verus vérifie statiquement que le code Rust exécutable satisfera toujours les spécifications pour toutes les exécutions possibles du code. Au lieu de vérifications au moment de l'exécution, Verus s'appuie sur des solveurs puissants pour prouver que le code est correct. Verus prend actuellement en charge un sous-ensemble de Rust (que nous nous efforçons d'étendre), et dans certains cas, il permet aux développeurs d'aller au-delà du système de types Rust standard et de vérifier statiquement l'exactitude du code qui, par exemple, manipule des pointeurs bruts. Verus est en développement actif ; des fonctionnalités peuvent être rompues et/ou manquantes, et la documentation est encore incomplète.