Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben. Das Tool, das das macht, heißt Model Checker, und für Rust ist der praktischste im Moment Kani, gebaut von AWS. Du schreibst normale Rust-Assertions. Kani verwandelt sie in mathematische Claims und prüft sie für jede mögliche Eingabe. Keine Theorembeweiser. Keine Proof Assistants. Keine sechsmonatige Reise durch Coq.

Der Haken ist, dass „jede mögliche Eingabe” nur funktioniert, wenn der Eingaberaum klein genug ist, um ihn erschöpfend zu durchsuchen. Wenn deine Funktion einen Vec<u8> mit einer Million Elementen nimmt, wird Kani nicht jede Permutation prüfen. Es prüft bis zu einer von dir angegebenen Grenze oder läuft, bis dein Laptop keinen RAM mehr hat. Der Beweis ist real, aber er ist beschränkt.

Was „Beweis ohne Beweise” wirklich bedeutet

Formale Verifikation bedeutet normalerweise, dein Programm in einem Proof Assistant wie Coq zu schreiben, Invarianten von Hand zu definieren und den Solver durch taktische Schritte zu führen. Ein verifizierter Compiler wie CompCert hat Jahre gedauert. Die meisten Teams haben keine Jahre.

Model Checking ist anders. Du schreibst normalen Rust. Du fügst eine Testfunktion mit der Annotation #[kani::proof] hinzu. Darin erzeugst du symbolische Werte mit kani::any(), rufst deinen Code auf und stellst Assertions auf. Kani kompiliert deinen Code zu einer logischen Formel und übergibt sie an einen SMT Solver. Der Solver bestätigt entweder, dass die Eigenschaft für alle Eingaben innerhalb der Grenze gilt, oder er liefert ein konkretes Gegenbeispiel.

Du hast keinen Beweis geschrieben. Du hast einen Test mit einem Universalquantor geschrieben. Das Tool hat den Beweis geschrieben.

Wie Kani Rust in Logik verwandelt

Kani ist ein Bounded Model Checker. Es entfaltet deinen Code in eine logische Formel und fragt einen SMT Solver, ob ein Ausführungspfad eine Assertion verletzen kann. Der Solver behandelt Variablen als symbolisch. Ein normaler Test gibt x den Wert 5. Ein Kani-Proof gibt x ein Symbol, das jede mögliche u32 repräsentiert.

Hier ist ein triviales Beispiel. Wir haben eine Funktion, die niemals überlaufen sollte, und wir wollen das beweisen.

// 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);
        }
    }
}

Führe cargo kani aus und Kani verifiziert das in Sekunden. Es prüft alle 4.294.967.296 möglichen Werte von x, ohne sie einzeln auszuführen. Der SMT Solver schließt aus der symbolischen Repräsentation, dass kein Gegenbeispiel existiert.

Das #[cfg(kani)]-Guard bedeutet, dass dieser Code nur unter Kani kompiliert. Es bläht deinen Release-Build nicht auf.

Ein echtes Beispiel: Einen Parser als crashfrei beweisen

Overflows sind einfach. Die interessanten Fälle sind datenabhängig. Nehmen wir an, wir haben eine Funktion, die einen kleinen protocol header parst. Wir wollen beweisen, dass sie niemals panict, egal welche Bytes wir ihr füttern.

// 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 verifiziert, dass parse_header niemals panict für jeden Eingabe-Buffer der Länge 0 bis 8. Es prüft den Bounds-Test, den Version-Check und den Array-Index-Zugriff. Hätten wir buf[1] geschrieben, statt zuerst die Länge zu prüfen, würde Kani ein Gegenbeispiel finden: ein 1-Byte-Buffer, bei dem buf[1] out of bounds ist.

Die #[kani::unwind(5)]-Annotation sagt Kani, wie oft es Schleifen entfalten soll. Da unsere Funktion keine Schleifen hat, ist das konservativ.

Das Bounding-Problem: Wo Model Checking an die Wand stößt

Model Checking ist erschöpfend innerhalb seiner Grenzen. Außerhalb dieser Grenzen sagt es nichts. Das ist der fundamentale Trade-off.

Schleifen sind die erste Wand. Kani muss jede Schleife eine feste Anzahl von Malen entfalten. Wenn deine Funktion über einen Vec iteriert und du die Unwind-Grenze auf 10 setzt, beweist Kani Korrektheit für Vektoren der Länge 0 bis 10. Es sagt nichts über Länge 11. Jede Erhöhung multipliziert den Zustandsraum. Ein Unwind von 50 könnte in Minuten fertig sein. Ein Unwind von 500 könnte überhaupt nicht fertig werden.

Rekursion ist ähnlich. Jeder Aufruf expandiert die Formel. Tiefe Rekursion explodiert den Speicherverbrauch.

Datengröße ist die zweite Wand. Kani kann gut mit Arrays fester Größe umgehen. Es hat Probleme mit dynamisch allozierten Collections, es sei denn, du begrenzt ihre Größe explizit.

Die Standard Library ist die dritte Wand. Kani modelliert viel davon, aber nicht alles. Wenn du etwas aufrufst, das Kani nicht versteht, schlägt der Beweis mit einer fehlenden Funktionsdefinition fehl.

Was Kani beweisen kann und wo es scheitert

Kani ist gut darin, Panics, Integer-Overflows und Assertion-Verletzungen in beschränktem Code zu finden. Es ist exzellent für kryptografische Primitive, protocol parser und kleine State Machines. Das sind Orte, wo eine einzelne schlechte Eingabe Katastrophe verursacht und der Code natürlich beschränkt ist.

Kani ist nicht gut darin, Liveness-Eigenschaften zu beweisen, wie „jede Anfrage bekommt irgendwann eine Antwort.” Das erfordert Reasoning über unendliche Ausführungen, was Bounded Model Checking explizit nicht tut. Für Liveness brauchst du einen temporalen Model Checker wie TLA+.

Kani ist auch kein Ersatz für Tests. Ein bestandener Beweis sagt dir, dass kein Gegenbeispiel innerhalb der Grenze existiert. Ein Test sagt dir, dass der Code sich für eine spezifische Eingabe korrekt verhält, die dir wichtig ist. Kani fängt die Edge Cases, an die du nicht gedacht hast. Tests fangen die Integrationsprobleme, die Kani nicht sehen kann.

Kani in CI laufen lassen, ohne die Runner zu schmelzen

Ein einzelner Kani-Proof für eine kleine Funktion dauert Sekunden. Eine Suite für eine echte Crate dauert Minuten. Ein Proof mit hohen Unwind-Grenzen kann Stunden dauern. Du willst nicht, dass deine CI-Pipeline auf einen zweistündigen SMT-Solve wartet.

Halte Kani-Proofs klein und schnell. Beweise die sicherheitskritischen Funktionen, diejenigen, bei denen ein Bug ein Vorfall ist. Versuche nicht, dein gesamtes Web-Framework zu beweisen. Setze ein Timeout, vielleicht fünf Minuten pro Proof, und behandle ein Timeout als Failure to Prove, nicht als Proof of Failure.

Hier ist ein Makefile-Pattern, das funktioniert:

# 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 läuft in CI bei jedem Pull Request. kani läuft nächtlich. Wenn ein Proof regressiert, erfährst du es innerhalb eines Tages, nicht nach dem Shipping.

Wenn du eine öffentliche API exponierst, schreibe einen Kani-Proof pro öffentlicher Funktion, die sie mit vollständig symbolischen Eingaben aufruft. Das ist das, was einem formalen Contract Test am nächsten kommt. Es beweist nicht, dass die Implementierung korrekt ist, aber es beweist, dass die Implementierung bei beliebigen validen Eingaben nicht crasht.

Wann man stattdessen zu einem echten Proof Assistant greifen sollte

Wenn du Eigenschaften über unbeschränkte Datenstrukturen beweisen musst, wie „diese Linked List ist immer azyklisch,” wird Kani dir nicht helfen. Die Unwind-Grenze macht die Aussage zunichte. Dafür brauchst du ein Tool wie Creusot, das Rust nach WhyML übersetzt und einen Proof Assistant verwendet. Es ist mehr Arbeit, aber es kann mit unbeschränkten Strukturen umgehen.

Wenn du Äquivalenzbeweise oder Undefined-Behavior-Detection brauchst, sitzen Tools wie MIRI oder KLEE an verschiedenen Punkten auf dem Effort-versus-Coverage-Spektrum. Kani ist der Sweet Spot für „Ich habe beschränkten Code und will wissen, ob er panict.” Parser, Decoder, Serializer und Konfigurations-Validator passen alle. Das Rust-Typensystem eliminiert bereits ganze Klassen von Bugs. Kani eliminiert diejenigen, die das Typensystem nicht erreichen kann.

Was zuerst zu versuchen ist

Wenn du eine Rust-Crate hast mit einer Funktion, die dich ängstigt, füge Kani hinzu. Die beängstigende Funktion ist normalerweise die, die untrusted Input parst, Bit-Manipulation macht oder in Arrays indiziert. Schreibe einen Proof Harness, der sie mit kani::any() aufruft. Führe cargo kani aus. Wenn es besteht, hast du einen beschränkten Beweis der Crash-Freiheit. Wenn es fehlschlägt, hast du ein konkretes Gegenbeispiel, das ein Bug-Report gewesen wäre.

Du musst keine neue Sprache lernen. Du musst Sequenzenkalkül nicht verstehen. Du schreibst Rust-Assertions, und ein Solver sagt dir, ob sie gelten. Das ist kein formaler Beweis im akademischen Sinn. Es ist ein mechanischer Beweis im praktischen Sinn, und für die meiste Software ist praktisch genau das, was du brauchst.

Häufig gestellte Fragen

Was ist Model Checking in der Software-Verifikation?

Model Checking ist eine automatisierte Technik, die alle möglichen Zustände eines Systems erschöpfend erkundet, um zu verifizieren, ob spezifizierte Eigenschaften gelten. Für Rust verwenden Tools wie Kani Bounded Model Checking, um Assertions über alle möglichen Eingaben innerhalb definierter Grenzen zu beweisen, ohne manuelle Beweiskonstruktion zu erfordern.

Wie unterscheidet sich Kani vom Schreiben von Unit Tests?

Ein Unit Test prüft eine spezifische Eingabe. Ein Kani-Proof prüft jede Eingabe innerhalb einer Grenze. Wenn ein Kani-Proof besteht, weißt du, dass kein Gegenbeispiel innerhalb des beschränkten Zustandsraums existiert. Der Beweis ist stärker, aber er ist durch die von dir gesetzten Grenzen limitiert.

Kann Kani beweisen, dass meine gesamte Rust-Anwendung korrekt ist?

Nein. Kani funktioniert am besten bei kleinen, beschränkten Funktionen. Der Zustandsraum wächst exponentiell mit Schleifeniterationen, Rekursionstiefe und Datengröße. Verwende Kani für sicherheitskritische Komponenten wie Parser und protocol handler, nicht für Anwendungslogik.

Was passiert, wenn Kani auf eine Schleife ohne feste Grenze trifft?

Kani benötigt eine Unwind-Grenze für Schleifen. Wenn die Schleife mehr ausführen könnte, als die Grenze erlaubt, fügt Kani eine Unwinding-Assertion ein, die fehlschlägt. Du musst entweder die Grenze erhöhen oder den Code so refactoren, dass er eine statisch bekannte Iterationsanzahl hat. Das ist die Hauptlimitation von Bounded Model Checking.