Verus : vérifier formellement la correction du code Rust avec des preuves automatisées
En bref
- Verus est un vérificateur de programme open-source qui prouve mathématiquement la correction du code Rust en le confrontant à des spécifications formelles, bien au-delà du test traditionnel.
- Les développeurs annotent directement le code Rust avec des préconditions et postconditions en syntaxe Rust, recevant des retours en moins d'une seconde.
- Amazon utilise Verus pour certifier des composants critiques du Nitro Isolation Engine et d'autres infrastructures clés.
Ce que dit la source
Amazon Science présente Verus comme une solution au problème que Rust, malgré sa solidité, ne garantit pas la correction du programme : le type system prévient des classes de bugs, mais n'empêche pas un algorithme correct de mal coder sa logique ou de vérifier ses invariants. Verus permet aux développeurs d'annoter le code avec des spécifications mathématiques (préconditions, postconditions, boucles invariantes) et vérifie automatiquement que le code respecte ces spécifications pour tous les inputs possibles, pas seulement les cas testés. L'outil gère automatiquement les étapes de preuve, le développeur guidant les grandes lignes (structure inductive, etc.), voire des IA assistant à la génération de preuves.
- Verus accepte des spécifications en syntaxe Rust native, avec `requires` et `ensures`, directement dans les annotations du source ; les compilateurs Rust standard ignorent ces annotations, donc le code annoté reste compatible.
- Applicable aux blocs `unsafe` et au code concurrent avec verrous personnalisés, rétablissant des garanties de sécurité vérifiées mécaniquement pour les implémentations critiques de performance.
- Amazon l'a utilisé pour certifier des primitives clés du Nitro Isolation Engine (hyperviseur AWS) et d'autres composants critiques d'infrastructure.
- Retours rapides : la vérification s'exécute en moins d'une seconde, permettant des boucles feedback interactives et l'assistance d'agents IA dans la génération de preuves.
- Adoption dans des projets open-source : validateurs de certificats, parsers de formats de données, contrôleurs Kubernetes.
Dans les commentaires
Débat partagé : intérêt affirmé chez les développeurs ouverts à la vérification formelle, résistance exprimée sur la viabilité des annotations humaines, demandes pratiques sur l'outillage concurrent et la comparaison avec des outils existants (TLA+, Miri, Kani, Creusot, Dafny).
- Plusieurs commentateurs mentionnent des outils concurrents aux objectifs proches : Miri, Kani, Creusot, TLA+, Dafny, Aeneas (Microsoft, basé sur Lean), Whiley. Un point récurrent : les relations et distinctions entre ces outils ne sont pas claires publiquement.
- Un commentateur soulève le paradoxe classique de la vérification formelle : si les humains ne peuvent pas écrire de code correct, comment peuvent-ils écrire des preuves correctes ? Il concède cependant que les LLM pourraient changer cette donne en générant les annotations.
- Demandes pratiques non traitées dans la source : exemple concret de vérification de code concurrent, applicabilité en .NET/C# avec annotations (contrairement à Dafny qui impose un langage distinct), utilité réelle pour les bugs récents d'Ubuntu Coreutils.
- Un commentateur note que l'article manque d'exemple de vérification concurrent, la rendant difficile à visualiser au-delà de la recherche binaire.
- Question théorique : si Verus prouve la sécurité du code `unsafe`, pourquoi Rust a-t-il encore besoin du mot-clé `unsafe` ? (La question reste sans réponse directe dans le fil.)
Alternatives citées : Kani (AWS, model-checking Rust), Creusot (vérification Rust), Miri (interpréteur Rust runtime), TLA+ (spécification de systèmes distribués, hors-compilation), Dafny (vérification, langage dédié), Aeneas (Microsoft, basé sur Lean).
Notre lecture
Verus remplit un créneau réel : pour du code Rust critique (et unsafe), passer de « probablement correct » à « prouvé correct » a une valeur concrète en sécurité, notamment chez Amazon sur l'isolation des VMs. Le retrait de friction majeure : c'est l'écosystème des outils de vérification pour Rust qui devient confus pour l'adoptant, avec plusieurs solutions concurrentes (Kani, Creusot, Miri) sans consensus public sur leurs différences et cas d'usage respectifs. La viabilité dépendra aussi de la qualité réelle des assistants IA pour générer les annotations (la théorie est séduisante, la pratique à l'échelle l'est moins). À surveiller pour les équipes travaillant sur du code critique Rust, mais probablement pas une adoption de masse court terme ; l'absence de comparaisons publiques transparentes avec Kani et Creusot reste un frein à la compréhension de ce qui est vraiment distinct ici.