Vous pouvez prouver votre code Rust correct sans écrire une seule preuve. L’outil qui le fait s’appelle un model checker, et pour Rust le plus pratique en ce moment est Kani, construit par AWS. Vous écrivez des assertions Rust normales. Kani les transforme en claims mathématiques et les vérifie pour chaque entrée possible. Pas de theorem provers. Pas de proof assistants. Pas de détour de six mois dans Coq.

Le hic est que “chaque entrée possible” ne fonctionne que quand l’espace d’entrées est assez petit pour être épuisé. Si votre fonction prend un Vec<u8> d’un million d’éléments, Kani ne vérifiera pas chaque permutation. Il vérifiera jusqu’à une borne que vous spécifiez, ou tournera jusqu’à ce que votre portable manque de RAM. La preuve est réelle, mais elle est bornée.

Ce que signifie réellement “preuve sans preuves”

La vérification formelle signifie habituellement écrire votre programme dans un proof assistant comme Coq, définir les invariants à la main, et guider le solver à travers des étapes tactiques. Un compilateur vérifié comme CompCert a pris des années. La plupart des équipes n’ont pas des années.

Le model checking est différent. Vous écrivez du Rust normal. Vous ajoutez une fonction de test annotée avec #[kani::proof]. À l’intérieur, vous créez des valeurs symboliques avec kani::any(), appelez votre code, et faites des assertions. Kani compile votre code en une formule logique et la passe à un SMT solver. Le solver confirme soit que la propriété tient pour toutes les entrées dans la borne, soit il produit un contre-exemple concret.

Vous n’avez pas écrit de preuve. Vous avez écrit un test avec un quantificateur universel. L’outil a écrit la preuve.

Comment Kani transforme Rust en logique

Kani est un bounded model checker. Il déroule votre code en une formule logique et demande à un SMT solver si un chemin d’exécution peut violer une assertion. Le solver traite les variables comme symboliques. Un test normal donne à x la valeur 5. Une preuve Kani donne à x un symbole qui représente chaque u32 possible.

Voici un exemple trivial. Nous avons une fonction qui ne devrait jamais déborder, et nous voulons le prouver.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

Lancez cargo kani et Kani vérifie cela en quelques secondes. Il vérifie les 4 294 967 296 valeurs possibles de x sans les exécuter une par une. Le SMT solver raisonne sur la représentation symbolique et conclut qu’aucun contre-exemple n’existe.

Le guard #[cfg(kani)] signifie que ce code ne se compile que sous Kani. Il n’alourdit pas votre release build.

Un exemple réel : prouver qu’un parser ne crashe jamais

Les débordements sont faciles. Les cas intéressants dépendent des données. Disons que nous avons une fonction qui parse un petit header de protocole. Nous voulons prouver qu’elle ne panic jamais, peu importe les bytes que nous lui donnons.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani vérifie que parse_header ne panic jamais pour n’importe quel buffer d’entrée de longueur 0 à 8. Il vérifie le test de bounds, le check de version et l’indexation du tableau. Si nous avions écrit buf[1] au lieu de vérifier la longueur d’abord, Kani trouverait un contre-exemple : un buffer d’1 byte où buf[1] est hors bounds.

L’annotation #[kani::unwind(5)] dit à Kani combien de fois dérouler les boucles. Comme notre fonction n’a pas de boucles, c’est conservateur.

Le problème du bounding : où le model checking heurte le mur

Le model checking est exhaustif dans ses bornes. En dehors de ces bornes, il ne dit rien. C’est le trade-off fondamental.

Les boucles sont le premier mur. Kani doit dérouler chaque boucle un nombre fixe de fois. Si votre fonction itère sur un Vec et que vous mettez la borne de unwind à 10, Kani prouve la correction pour des vecteurs de longueur 0 à 10. Il ne dit rien sur la longueur 11. Chaque incrément multiplie l’espace d’états. Un unwind de 50 pourrait finir en minutes. Un unwind de 500 pourrait ne jamais finir.

La récursion est similaire. Chaque appel expande la formule. Une récursion profonde fait exploser l’utilisation mémoire.

La taille des données est le deuxième mur. Kani gère bien les tableaux de taille fixe. Il peine avec les collections allouées dynamiquement à moins que vous ne borniez leur taille explicitement.

La standard library est le troisième mur. Kani modélise une grande partie, mais pas tout. Si vous appelez quelque chose que Kani ne comprend pas, la preuve échoue avec une définition de fonction manquante.

Ce que Kani peut prouver et où il échoue

Kani est bon pour trouver des panics, des débordements d’entiers et des violations d’assertions dans du code borné. Il est excellent pour les primitives cryptographiques, les parsers de protocole et les petites state machines. Ce sont des endroits où une seule mauvaise entrée cause une catastrophe, et le code est naturellement borné.

Kani n’est pas bon pour prouver des propriétés de liveness, comme “chaque requête reçoit finalement une réponse.” Cela nécessite de raisonner sur des exécutions infinies, ce que le bounded model checking ne fait pas explicitement. Pour la liveness, vous voulez un temporal model checker comme TLA+.

Kani n’est pas non plus un remplacement pour les tests. Une preuve qui passe vous dit qu’aucun contre-exemple n’existe dans la borne. Un test vous dit que le code se comporte correctement pour une entrée spécifique qui vous importe. Kani attrape les edge cases auxquels vous n’avez pas pensé. Les tests attrapent les problèmes d’intégration que Kani ne peut pas voir.

Faire tourner Kani en CI sans faire fondre vos runners

Une seule preuve Kani sur une petite fonction prend des secondes. Une suite sur une vraie crate prend des minutes. Une preuve avec des bornes de unwind élevées peut prendre des heures. Vous ne voulez pas que votre pipeline CI attende un solve SMT de deux heures.

Gardez les preuves Kani petites et rapides. Prouvez les fonctions safety-critical, celles où un bug est un incident. N’essayez pas de prouver tout votre web framework. Mettez un timeout, peut-être cinq minutes par preuve, et traitez un timeout comme un failure to prove, pas comme un proof of failure.

Voici un pattern de Makefile qui fonctionne :

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast tourne en CI à chaque pull request. kani tourne chaque nuit. Si une preuve régresse, vous le savez dans la journée, pas après le shipping.

Si vous exposez une API publique, écrivez une preuve Kani par fonction publique qui l’appelle avec des entrées entièrement symboliques. C’est la chose la plus proche d’un formal contract test. Cela ne prouve pas que l’implémentation est correcte, mais cela prouve que l’implémentation ne crashe pas sur des entrées valides arbitraires.

Quand se tourner vers un vrai proof assistant

Si vous devez prouver des propriétés sur des structures de données non bornées, comme “cette linked list est toujours acyclique,” Kani ne vous aidera pas. La borne de unwind défait le claim. Pour cela, vous avez besoin d’un outil comme Creusot, qui traduit Rust vers WhyML et utilise un proof assistant. C’est plus de travail, mais il gère les structures non bornées.

Si vous avez besoin de preuves d’équivalence ou de détection d’undefined behavior, des outils comme MIRI ou KLEE se situent à différents points sur le spectre effort-versus-coverage. Kani est le sweet spot pour “j’ai du code borné et je veux savoir s’il panic.” Les parsers, decoders, serializers et validateurs de configuration conviennent tous. Le système de types de Rust élimine déjà des classes entières de bugs. Kani élimine ceux que le système de types ne peut pas atteindre.

Quoi essayer d’abord

Si vous avez une crate Rust avec une fonction qui vous effraie, ajoutez Kani. La fonction effrayante est généralement celle qui parse de l’untrusted input, fait de la manipulation de bits ou indexe dans des tableaux. Écrivez un proof harness qui l’appelle avec kani::any(). Lancez cargo kani. Si ça passe, vous avez une preuve bornée de liberté de crash. Si ça échoue, vous avez un contre-exemple concret qui aurait été un bug report.

Vous n’avez pas besoin d’apprendre un nouveau langage. Vous n’avez pas besoin de comprendre le calcul des séquents. Vous écrivez des assertions Rust, et un solver vous dit si elles tiennent. Ce n’est pas une preuve formelle au sens académique. C’est une preuve mécanique au sens pratique, et pour la plupart des logiciels, pratique est exactement ce dont vous avez besoin.

Questions fréquemment posées

Qu’est-ce que le model checking en vérification de logiciel ?

Le model checking est une technique automatisée qui explore exhaustivement tous les états possibles d’un système pour vérifier si les propriétés spécifiées tiennent. Pour Rust, des outils comme Kani utilisent le bounded model checking pour prouver des assertions sur toutes les entrées possibles dans des limites définies, sans nécessiter de construction manuelle de preuves.

En quoi Kani diffère-t-il de l’écriture de unit tests ?

Un unit test vérifie une entrée spécifique. Une preuve Kani vérifie chaque entrée dans une borne. Si une preuve Kani passe, vous savez qu’aucun contre-exemple n’existe dans l’espace d’états borné. La preuve est plus forte, mais elle est limitée par les bornes que vous fixez.

Kani peut-il prouver que toute mon application Rust est correcte ?

Non. Kani fonctionne mieux sur des petites fonctions bornées. L’espace d’états croît exponentiellement avec les itérations de boucles, la profondeur de récursion et la taille des données. Utilisez Kani pour des composants safety-critical comme les parsers et les handlers de protocole, pas pour la logique applicative.

Que se passe-t-il quand Kani rencontre une boucle sans borne fixe ?

Kani nécessite une borne de unwind pour les boucles. Si la boucle pourrait s’exécuter plus de fois que la borne ne le permet, Kani insère une unwinding assertion qui échoue. Vous devez soit augmenter la borne, soit refactoriser le code pour avoir un nombre d’itérations connu statiquement. C’est la principale limitation du bounded model checking.