Vous n’avez pas besoin de LTL pour utiliser un model checker

Vous n’avez pas besoin d’apprendre la logique temporelle linéaire pour utiliser un model checker. Des outils comme Kani, CBMC et Alloy vous permettent de vérifier des propriétés avec des assertions et des contraintes relationnelles ordinaires. Vous échangez la capacité de prouver des propriétés de liveness contre une courbe d’apprentissage mesurée en heures plutôt qu’en semaines, et pour la plupart des bugs logiciels, c’est un échange qui vaut la peine.

La temporal logic est le gardien que la plupart des model checkers exigent

Les model checkers classiques, SPIN et NuSMV, vous demandent d’exprimer des propriétés en LTL ou CTL. Vous écrivez des choses comme G(request -> F(response)) pour signifier : « globalement, chaque requête est éventuellement suivie d’une réponse ». C’est puissant. Cela peut prouver que votre protocole ne se bloque jamais en deadlock, que chaque message est éventuellement acquitté, que votre système est fair.

C’est aussi une compétence spécialisée que la plupart des développeurs en activité ne possèdent pas. Lire une formule LTL n’est pas comme lire du code. Les opérateurs sont modaux, la sémantique porte sur des traces infinies, et l’intuition que vous avez développée en écrivant des unit tests ne se transpose pas. La question est donc légitime : si vous voulez la puissance de bug-finding du model checking, devez-vous vraiment gravir cette montagne d’abord ?

Non. Une classe différente d’outils existe depuis des décennies, et elle vérifie le code avec les mêmes assertions que vous écrivez déjà.

Les bounded model checkers transforment les assertions en problèmes SAT

Les bounded model checkers ne vous demandent pas d’apprendre une nouvelle logique. Ils vous demandent d’écrire un test harness. Vous déclarez des inputs non déterministes, les contrainez avec des assumptions et affirmez des propriétés dans le langage hôte. L’outil déroule ensuite les boucles jusqu’à une borne, encode le programme comme une formule SAT ou SMT, et demande au solver de trouver un counterexample.

Si le solver renvoie UNSAT, votre propriété est vérifiée pour tous les paths dans cette borne. S’il trouve un counterexample, vous obtenez un trace concret montrant exactement quels inputs déclenchent le bug. Pas d’opérateurs temporels. Pas de traces infinies. Juste une assertion échouée avec un vecteur d’input reproductible.

Kani est le bounded model checker le plus accessible pour Rust. Il s’installe avec cargo install kani-verifier et fonctionne sur du code Rust ordinaire.

Un exemple réel : vérifier une state machine en Rust

Voici une state machine avec un bug. Elle suit un compteur simple qui décrémente à chaque tick jusqu’à atteindre zéro, puis repasse en idle.

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

Le bug est subtil. Regardez stop. Il met l’état à Stopped mais laisse count inchangé. Si quelque chose suppose plus tard que count == 0 quand state == State::Stopped, cette assumption est fausse.

Voici un Kani proof harness qui le détecte :

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani explore chaque path. Il constate que si initial == 2, après start la machine est Running avec count == 2. Un tick décrémente count à 1 mais l’état reste Running. Puis stop met l’état à Stopped avec count == 1. L’assertion échoue. Kani rapporte ce trace exact.

C’est l’expérience du model checking sans temporal logic. Vous écrivez du Rust. Vous écrivez des assertions en Rust. L’outil vous dit quels inputs les cassent.

Alloy trouve des bugs au niveau design avec la logique relationnelle

Les bounded model checkers vérifient le code. Alloy vérifie les designs.

Alloy est un model finder, pas un model checker traditionnel, mais la distinction importe moins que le workflow. Vous décrivez votre système comme un ensemble de relations, les invariants d’état comme des contraintes en first-order logic, et demandez à Alloy de trouver un counterexample. Il cherche toutes les instances possibles jusqu’à une scope définie par l’utilisateur et vous montre des diagrammes de l’échec.

Voici un modèle Alloy d’une propriété de graphe orienté simple :

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

L’assertion affirme que la reachability est symétrique. Alloy vérifie ceci pour tous les graphes d’au plus trois nœuds et dessine immédiatement un counterexample : un graphe où n1 pointe vers n2 mais n2 n’a pas d’arêtes sortantes. Aucun opérateur G, F ou U n’apparaît nulle part.

Ce que vous abandonnez : liveness et comportement infini

Cette commodité a un coût. Les bounded model checkers ne vérifient le comportement que jusqu’à une borne de boucle ou une longueur de trace. Ils ne peuvent pas prouver qu’une requête est éventuellement répondue, seulement que de mauvaises choses n’arrivent pas dans les N premières étapes. Alloy ne vérifie que les instances dans sa scope. Il ne peut pas prouver de propriétés pour des systèmes arbitrairement grands, seulement qu’aucun counterexample n’existe sous la borne.

Si vous devez prouver que votre protocole de consensus ne perd jamais de writes commités, ou que chaque message est éventuellement livré, vous avez encore besoin de temporal logic et d’unbounded model checking. Des outils comme TLA+ enrobent la temporal logic dans une syntaxe qui ressemble plus aux mathématiques qu’à la logique modale, mais la sémantique sous-jacente reste temporelle.

Pour les invariants de structures de données, l’enforcement de contrats d’API et la recherche de la race condition qui ne se déclenche que sur le 47ème path d’exécution, les outils bounded sont généralement suffisants. Ils attrapent les bugs que les unit tests ratent, et ils le font avec des assertions que vous pouvez lire sans manuel.

Démarrer avec Kani en cinq minutes

Si vous avez Rust installé, le bounded model checking est à une commande près.

cargo install kani-verifier
cargo kani setup

Créez une nouvelle crate, écrivez une fonction avec un bug subtil, et ajoutez un harness #[kani::proof]. Lancez cargo kani. Si Kani trouve un counterexample, il affiche les inputs concrets qui déclenchent l’échec. S’il rapporte VERIFICATION SUCCESSFUL, votre propriété est vérifiée pour tous les paths dans les bornes par défaut.

Commencez par des fonctions qui ont des espaces d’état petits et des invariants clairs. Les state machines, la validation de parsers et les transitions d’état de protocoles sont des cibles idéales pour commencer. Évitez d’essayer de vérifier un serveur HTTP entier dès votre premier essai. Le SAT solver a des limites, et votre patience aussi.

FAQ : bounded vs. unbounded, liveness et par où commencer

Le bounded model checking est-il vraiment du model checking ?

Techniquement, c’est une variante qui encode le problème comme une satisfiability query plutôt que d’explorer le state graph explicitement. Pour un développeur qui essaie de trouver des bugs, la distinction est académique. Il explore tous les paths systématiquement, ce qui est ce que signifie le model checking en pratique.

Puis-je prouver la liveness avec Kani ou CBMC ?

Pas directement. Les propriétés de liveness nécessitent de raisonner sur un comportement infini, et les outils bounded limitent explicitement leur recherche. Vous pouvez parfois encoder une vérification de liveness bounded en déroulant assez d’étapes pour atteindre un fixpoint, mais c’est une technique avancée.

Et TLA+ ? Exige-t-il la temporal logic ?

TLA+ utilise la Temporal Logic of Actions, donc oui, techniquement. Mais Leslie Lamport a conçu la syntaxe pour qu’elle se lise comme des mathématiques ordinaires. La plupart des spécifications TLA+ passent 90% de leur texte sur des invariants d’état et des contraintes de structures de données, pas sur des opérateurs temporels. C’est le chemin le plus accessible si vous avez besoin de raisonnement temporel unbounded.

Devrais-je utiliser Alloy ou Kani ?

Utilisez Kani si vous avez du code Rust et voulez vérifier les détails d’implémentation. Utilisez Alloy si vous êtes encore en train de concevoir le système et voulez explorer si vos invariants sont même possibles avant d’écrire le code.

Choisissez l’outil qui correspond à votre problème, pas à votre ambition

La temporal logic est belle et puissante, mais elle n’est pas un prérequis pour la vérification formelle. Les bounded model checkers et les relational model finders vous permettent d’exprimer des propriétés dans les langues que vous connaissez déjà. Ils ne prouveront pas que votre système termine éventuellement, mais ils trouveront l’erreur off-by-one qui corrompt votre state machine de base de données. Pour la plupart des équipes, c’est le bug qui compte.

Commencez avec Kani sur une seule fonction à état. Écrivez une assertion. Laissez le solver vous dire ce que vous avez manqué.