Sie brauchen kein LTL, um einen Model Checker zu nutzen

Sie müssen keine lineare temporale Logik lernen, um einen Model Checker zu verwenden. Tools wie Kani, CBMC und Alloy ermöglichen die Verifikation von Eigenschaften mit gewöhnlichen Assertions und relationalen Constraints. Sie geben die Fähigkeit auf, Liveness-Eigenschaften zu beweisen, dafür ist die Lernkurve auf Stunden statt Wochen gemessen – und für die meisten Software-Bugs ist das ein lohnender Tausch.

Temporal Logic ist der Gatekeeper, den die meisten Model Checker verlangen

Die klassischen Model Checker, SPIN und NuSMV, verlangen, dass Sie Eigenschaften in LTL oder CTL formulieren. Sie schreiben Dinge wie G(request -> F(response)), was bedeutet: „Global gilt: Jede Anfrage wird irgendwann von einer Antwort gefolgt.“ Das ist mächtig. Es kann beweisen, dass Ihr protocol niemals in einen Deadlock gerät, dass jede Nachricht irgendwann bestätigt wird, dass Ihr System fair ist.

Es ist auch eine spezialisierte Fähigkeit, die die meisten aktiven Entwickler nicht haben. Eine LTL-Formel zu lesen ist nicht wie Code zu lesen. Die Operatoren sind modal, die Semantik basiert auf unendlichen Traces, und die Intuition, die Sie beim Schreiben von Unit-Tests aufgebaut haben, lässt sich nicht übertragen. Die Frage ist also berechtigt: Wenn Sie die Bug-finding-Power von Model Checking nutzen wollen, müssen Sie wirklich zuerst diesen Berg erklimmen?

Nein. Eine andere Klasse von Tools gibt es seit Jahrzehnten, und sie verifizieren Code mit denselben Assertions, die Sie bereits schreiben.

Bounded Model Checker verwandeln Assertions in SAT-Probleme

Bounded Model Checker verlangen nicht, dass Sie eine neue Logik lernen. Sie verlangen, dass Sie einen Test-Harness schreiben. Sie deklarieren nichtdeterministische Inputs, beschränken sie mit Assumptions und formulieren Eigenschaften in der Host-Sprache. Das Tool entrollt dann Schleifen bis zu einer Grenze, kodiert das Programm als SAT- oder SMT-Formel und bittet den Solver, ein Counterexample zu finden.

Wenn der Solver UNSAT zurückgibt, gilt Ihre Eigenschaft für alle Pfade innerhalb dieser Grenze. Wenn er ein Counterexample findet, erhalten Sie einen konkreten Trace, der genau zeigt, welche Inputs den Bug auslösen. Keine temporalen Operatoren. Keine unendlichen Traces. Einfach eine fehlgeschlagene Assertion mit einem reproduzierbaren Input-Vektor.

Kani ist der zugänglichste Bounded Model Checker für Rust. Er lässt sich mit cargo install kani-verifier installieren und funktioniert mit gewöhnlichem Rust-Code.

Ein echtes Beispiel: Überprüfung einer State Machine in Rust

Hier ist eine State Machine mit einem Bug. Sie verfolgt einen einfachen Counter, der bei jedem Tick dekrementiert, bis er Null erreicht, und wechselt dann zurück in den Idle-Zustand.

#[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;
        }
    }
}

Der Bug ist subtil. Sehen Sie sich stop an. Es setzt den Zustand auf Stopped, lässt count jedoch unverändert. Wenn später etwas annimmt, dass count == 0 wenn state == State::Stopped, ist diese Annahme falsch.

Hier ist ein Kani-Proof-Harness, der ihn aufdeckt:

#[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 erkundet jeden Pfad. Es stellt fest, dass wenn initial == 2, nach start die Maschine Running mit count == 2 ist. Ein tick dekrementiert count auf 1, aber der Zustand bleibt Running. Dann setzt stop den Zustand auf Stopped mit count == 1. Die Assertion schlägt fehl. Kani meldet diesen genauen Trace.

Das ist das Model-Checking-Erlebnis ohne Temporal Logic. Sie schreiben Rust. Sie schreiben Assertions in Rust. Das Tool sagt Ihnen, welche Inputs sie brechen.

Alloy findet Design-Level-Bugs mit relationaler Logik

Bounded Model Checker verifizieren Code. Alloy verifiziert Designs.

Alloy ist ein Model Finder, kein traditioneller Model Checker, aber der Unterschied ist weniger wichtig als der Workflow. Sie beschreiben Ihr System als Menge von Relationen, Zustands-Invarianten als Constraints der ersten Ordnung und bitten Alloy, ein Counterexample zu finden. Es durchsucht alle möglichen Instanzen bis zu einem vom Benutzer definierten Scope und zeigt Ihnen Diagramme des Fehlers.

Hier ist ein Alloy-Modell einer einfachen gerichteten Graph-Eigenschaft:

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

Die Assertion behauptet, dass Erreichbarkeit symmetrisch ist. Alloy prüft dies für alle Graphen von bis zu drei nodes und zeichnet sofort ein Counterexample: einen Graphen, in dem n1 auf n2 zeigt, n2 jedoch keine ausgehenden Kanten hat. Nirgends tauchen G, F oder U-Operatoren auf.

Was Sie aufgeben: Liveness und unendliches Verhalten

Dieser Komfort hat einen Preis. Bounded Model Checker verifizieren nur das Verhalten bis zu einer Schleifengrenze oder Trace-Länge. Sie können nicht beweisen, dass eine Anfrage irgendwann beantwortet wird, sondern nur, dass keine schlechten Dinge in den ersten N Schritten passieren. Alloy prüft nur Instanzen innerhalb seines Scopes. Es kann keine Eigenschaften für beliebig große Systeme beweisen, sondern nur, dass kein Counterexample unter der Grenze existiert.

Wenn Sie beweisen müssen, dass Ihr consensus protocol niemals committed writes verliert, oder dass jede Nachricht irgendwann zugestellt wird, brauchen Sie immer noch Temporal Logic und unbounded Model Checking. Tools wie TLA+ verpacken Temporal Logic in einer Syntax, die eher nach Mathematik als nach modaler Logik aussieht, aber die zugrundeliegende Semantik ist immer noch temporal.

Für Datenstruktur-Invarianten, API-Contract-Enforcement und das Finden der Race Conditions, der nur beim 47. Ausführungspfad ausgelöst wird, sind bounded Tools in der Regel ausreichend. Sie fangen die Bugs, die Unit-Tests verpassen, und sie tun es mit Assertions, die Sie ohne Lehrbuch lesen können.

Kani in fünf Minuten starten

Wenn Sie Rust installiert haben, ist Bounded Model Checking nur einen Befehl entfernt.

cargo install kani-verifier
cargo kani setup

Erstellen Sie eine neue Crate, schreiben Sie eine Funktion mit einem subtilen Bug und fügen Sie einen #[kani::proof]-Harness hinzu. Führen Sie cargo kani aus. Wenn Kani ein Counterexample findet, gibt es die konkreten Inputs aus, die den Fehler auslösen. Wenn es VERIFICATION SUCCESSFUL meldet, gilt Ihre Eigenschaft für alle Pfade innerhalb der Standard-Grenzen.

Starten Sie mit Funktionen, die kleine State Spaces und klare Invarianten haben. State Machines, Parser-Validierung und protocol state transitions sind ideale erste Ziele. Versuchen Sie nicht, gleich einen ganzen HTTP-Server zu verifizieren. Der SAT-Solver hat Grenzen, und Ihre Geduld auch.

FAQ: Bounded vs. Unbounded, Liveness und wo anfangen

Ist bounded model checking eigentlich model checking?

Technisch gesehen ist es eine Variante, die das Problem als Satisfiability-Query kodiert, anstatt den State Graph explizit zu erkunden. Für einen Entwickler, der Bugs finden will, ist der Unterschied akademisch. Es erkundet alle Pfade systematisch, was Model Checking in der Praxis bedeutet.

Kann ich Liveness mit Kani oder CBMC beweisen?

Nicht direkt. Liveness-Eigenschaften erfordern Reasoning über unendliches Verhalten, und bounded Tools begrenzen ihre Suche explizit. Sie können manchmal einen bounded Liveness-Check kodieren, indem Sie genug Schritte entrollen, um einen Fixpoint zu erreichen, aber das ist eine fortgeschrittene Technik.

Was ist mit TLA+? Verlangt es Temporal Logic?

TLA+ verwendet die Temporal Logic of Actions, also ja, technisch gesehen. Aber Leslie Lamport entwarf die Syntax so, dass sie wie gewöhnliche Mathematik liest. Die meisten TLA+-Spezifikationen verbringen 90% ihres Textes mit Zustands-Invarianten und Datenstruktur-Constraints, nicht mit temporalen Operatoren. Es ist der zugänglichste Weg, wenn Sie unbounded temporal reasoning brauchen.

Sollte ich Alloy oder Kani verwenden?

Verwenden Sie Kani, wenn Sie Rust-Code haben und Implementierungsdetails verifizieren wollen. Verwenden Sie Alloy, wenn Sie noch dabei sind, das System zu designen und erkunden wollen, ob Ihre Invarianten überhaupt möglich sind, bevor Sie Code schreiben.

Wählen Sie das Tool, das zu Ihrem Problem passt, nicht zu Ihrem Ehrgeiz

Temporal Logic ist schön und mächtig, aber sie ist keine Voraussetzung für formale Verifikation. Bounded Model Checker und relationale Model Finder ermöglichen es Ihnen, Eigenschaften in den Sprachen zu formulieren, die Sie bereits kennen. Sie werden nicht beweisen, dass Ihr System irgendwann terminiert, aber sie werden den Off-by-One-Fehler finden, der Ihre Datenbank-State-Machine beschädigt. Für die meisten Teams ist das der Bug, der zählt.

Beginnen Sie mit Kani bei einer einzelnen zustandsbehafteten Funktion. Schreiben Sie eine Assertion. Lassen Sie den Solver Ihnen sagen, was Sie übersehen haben.